YES 4.6290000000000004
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ IFR
mainModule List
|
| ((union :: Eq a => [a] -> [a] -> [a]) :: Eq a => [a] -> [a] -> [a]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | _ _ [] | = | [] |
| deleteBy | eq x (y : ys) | = | if x `eq` y then ys else y : deleteBy eq x ys |
|
| | elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
| elem_by | _ _ [] | = | False |
| elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| | nubBy :: (a -> a -> Bool) -> [a] -> [a]
| nubBy | eq l | = |
| nubBy' l [] | where |
| nubBy' | [] _ | = | [] |
| nubBy' | (y : ys) xs | |
| | | elem_by eq y xs | = |
|
| | | otherwise | = |
|
|
|
|
|
|
| | union :: Eq a => [a] -> [a] -> [a]
|
| | unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
If Reductions:
The following If expression
if eq x y then ys else y : deleteBy eq x ys
is transformed to
| deleteBy0 | ys y eq x True | = ys |
| deleteBy0 | ys y eq x False | = y : deleteBy eq x ys |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule List
|
| ((union :: Eq a => [a] -> [a] -> [a]) :: Eq a => [a] -> [a] -> [a]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | _ _ [] | = | [] |
| deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
| |
| deleteBy0 | ys y eq x True | = | ys |
| deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
| | elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
| elem_by | _ _ [] | = | False |
| elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| | nubBy :: (a -> a -> Bool) -> [a] -> [a]
| nubBy | eq l | = |
| nubBy' l [] | where |
| nubBy' | [] _ | = | [] |
| nubBy' | (y : ys) xs | |
| | | elem_by eq y xs | = |
|
| | | otherwise | = |
|
|
|
|
|
|
| | union :: Eq a => [a] -> [a] -> [a]
|
| | unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
|
| ((union :: Eq a => [a] -> [a] -> [a]) :: Eq a => [a] -> [a] -> [a]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | vw vx [] | = | [] |
| deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
| |
| deleteBy0 | ys y eq x True | = | ys |
| deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
| | elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
| elem_by | vz wu [] | = | False |
| elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| | nubBy :: (a -> a -> Bool) -> [a] -> [a]
| nubBy | eq l | = |
| nubBy' l [] | where |
| nubBy' | [] vy | = | [] |
| nubBy' | (y : ys) xs | |
| | | elem_by eq y xs | = |
|
| | | otherwise | = |
|
|
|
|
|
|
| | union :: Eq a => [a] -> [a] -> [a]
|
| | unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Cond Reductions:
The following Function with conditions
| nubBy' | [] vy | = [] |
| nubBy' | (y : ys) xs |
| | | elem_by eq y xs | |
| | | otherwise | |
|
is transformed to
| nubBy' | [] vy | = nubBy'3 [] vy |
| nubBy' | (y : ys) xs | = nubBy'2 (y : ys) xs |
| nubBy'1 | y ys xs True | = nubBy' ys xs |
| nubBy'1 | y ys xs False | = nubBy'0 y ys xs otherwise |
| nubBy'0 | y ys xs True | = y : nubBy' ys (y : xs) |
| nubBy'2 | (y : ys) xs | = nubBy'1 y ys xs (elem_by eq y xs) |
| nubBy'3 | [] vy | = [] |
| nubBy'3 | yx yy | = nubBy'2 yx yy |
The following Function with conditions
is transformed to
| undefined0 | True | = undefined |
| undefined1 | | = undefined0 False |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule List
|
| ((union :: Eq a => [a] -> [a] -> [a]) :: Eq a => [a] -> [a] -> [a]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | vw vx [] | = | [] |
| deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
| |
| deleteBy0 | ys y eq x True | = | ys |
| deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
| | elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
| elem_by | vz wu [] | = | False |
| elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| | nubBy :: (a -> a -> Bool) -> [a] -> [a]
| nubBy | eq l | = |
| nubBy' l [] | where |
| nubBy' | [] vy | = | nubBy'3 [] vy |
| nubBy' | (y : ys) xs | = | nubBy'2 (y : ys) xs |
|
| nubBy'0 | y ys xs True | = | y : nubBy' ys (y : xs) |
|
| nubBy'1 | y ys xs True | = | nubBy' ys xs |
| nubBy'1 | y ys xs False | = | nubBy'0 y ys xs otherwise |
|
| nubBy'2 | (y : ys) xs | = | nubBy'1 y ys xs (elem_by eq y xs) |
|
| nubBy'3 | [] vy | = | [] |
| nubBy'3 | yx yy | = | nubBy'2 yx yy |
|
|
|
|
| | union :: Eq a => [a] -> [a] -> [a]
|
| | unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Let/Where Reductions:
The bindings of the following Let/Where expression
| nubBy' l [] |
| where |
| nubBy' | [] vy | = nubBy'3 [] vy |
| nubBy' | (y : ys) xs | = nubBy'2 (y : ys) xs |
|
|
| nubBy'0 | y ys xs True | = y : nubBy' ys (y : xs) |
|
|
| nubBy'1 | y ys xs True | = nubBy' ys xs |
| nubBy'1 | y ys xs False | = nubBy'0 y ys xs otherwise |
|
|
| nubBy'2 | (y : ys) xs | = nubBy'1 y ys xs (elem_by eq y xs) |
|
|
| nubBy'3 | [] vy | = [] |
| nubBy'3 | yx yy | = nubBy'2 yx yy |
|
are unpacked to the following functions on top level
| nubByNubBy' | yz [] vy | = nubByNubBy'3 yz [] vy |
| nubByNubBy' | yz (y : ys) xs | = nubByNubBy'2 yz (y : ys) xs |
| nubByNubBy'0 | yz y ys xs True | = y : nubByNubBy' yz ys (y : xs) |
| nubByNubBy'1 | yz y ys xs True | = nubByNubBy' yz ys xs |
| nubByNubBy'1 | yz y ys xs False | = nubByNubBy'0 yz y ys xs otherwise |
| nubByNubBy'3 | yz [] vy | = [] |
| nubByNubBy'3 | yz yx yy | = nubByNubBy'2 yz yx yy |
| nubByNubBy'2 | yz (y : ys) xs | = nubByNubBy'1 yz y ys xs (elem_by yz y xs) |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
mainModule List
|
| (union :: Eq a => [a] -> [a] -> [a]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
| deleteBy | vw vx [] | = | [] |
| deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
| |
| deleteBy0 | ys y eq x True | = | ys |
| deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
| | elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool
| elem_by | vz wu [] | = | False |
| elem_by | eq y (x : xs) | = | x `eq` y || elem_by eq y xs |
|
| | nubBy :: (a -> a -> Bool) -> [a] -> [a]
| nubBy | eq l | = | nubByNubBy' eq l [] |
|
| |
| nubByNubBy' | yz [] vy | = | nubByNubBy'3 yz [] vy |
| nubByNubBy' | yz (y : ys) xs | = | nubByNubBy'2 yz (y : ys) xs |
|
| |
| nubByNubBy'0 | yz y ys xs True | = | y : nubByNubBy' yz ys (y : xs) |
|
| |
| nubByNubBy'1 | yz y ys xs True | = | nubByNubBy' yz ys xs |
| nubByNubBy'1 | yz y ys xs False | = | nubByNubBy'0 yz y ys xs otherwise |
|
| |
| nubByNubBy'2 | yz (y : ys) xs | = | nubByNubBy'1 yz y ys xs (elem_by yz y xs) |
|
| |
| nubByNubBy'3 | yz [] vy | = | [] |
| nubByNubBy'3 | yz yx yy | = | nubByNubBy'2 yz yx yy |
|
| | union :: Eq a => [a] -> [a] -> [a]
|
| | unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| unionBy | eq xs ys | = | xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(zu7800), Succ(zu4500000)) → new_primPlusNat(zu7800, zu4500000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(zu7800), Succ(zu4500000)) → new_primPlusNat(zu7800, zu4500000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(zu3110000), Succ(zu450000)) → new_primMulNat(zu3110000, Succ(zu450000))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(zu3110000), Succ(zu450000)) → new_primMulNat(zu3110000, Succ(zu450000))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(zu311000), Succ(zu45000)) → new_primEqNat(zu311000, zu45000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(zu311000), Succ(zu45000)) → new_primEqNat(zu311000, zu45000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, app(ty_Maybe, gc), gd) → new_esEs(zu31101, zu4501, gc)
new_esEs2(:(zu31100, zu31101), :(zu4500, zu4501), app(app(ty_@2, bah), bba)) → new_esEs0(zu31100, zu4500, bah, bba)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, app(app(app(ty_@3, gg), gh), ha), gd) → new_esEs1(zu31101, zu4501, gg, gh, ha)
new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), app(app(ty_Either, ee), ef), df) → new_esEs3(zu31100, zu4500, ee, ef)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, app(app(ty_Either, hc), hd), gd) → new_esEs3(zu31101, zu4501, hc, hd)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, eh, app(app(ty_Either, ga), gb)) → new_esEs3(zu31102, zu4502, ga, gb)
new_esEs3(Right(zu31100), Right(zu4500), bdb, app(app(ty_Either, beb), bec)) → new_esEs3(zu31100, zu4500, beb, bec)
new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), cb, app(app(app(ty_@3, cf), cg), da)) → new_esEs1(zu31101, zu4501, cf, cg, da)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, eh, app(app(app(ty_@3, fd), ff), fg)) → new_esEs1(zu31102, zu4502, fd, ff, fg)
new_esEs3(Right(zu31100), Right(zu4500), bdb, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs1(zu31100, zu4500, bdf, bdg, bdh)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, eh, app(ty_[], fh)) → new_esEs2(zu31102, zu4502, fh)
new_esEs3(Left(zu31100), Left(zu4500), app(app(app(ty_@3, bcd), bce), bcf), bca) → new_esEs1(zu31100, zu4500, bcd, bce, bcf)
new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), cb, app(app(ty_Either, dc), dd)) → new_esEs3(zu31101, zu4501, dc, dd)
new_esEs(Just(zu31100), Just(zu4500), app(ty_Maybe, ba)) → new_esEs(zu31100, zu4500, ba)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, eh, app(app(ty_@2, fb), fc)) → new_esEs0(zu31102, zu4502, fb, fc)
new_esEs3(Left(zu31100), Left(zu4500), app(app(ty_Either, bch), bda), bca) → new_esEs3(zu31100, zu4500, bch, bda)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), app(app(ty_@2, hf), hg), eh, gd) → new_esEs0(zu31100, zu4500, hf, hg)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, app(ty_[], hb), gd) → new_esEs2(zu31101, zu4501, hb)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), app(ty_Maybe, he), eh, gd) → new_esEs(zu31100, zu4500, he)
new_esEs2(:(zu31100, zu31101), :(zu4500, zu4501), app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs1(zu31100, zu4500, bbb, bbc, bbd)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), app(app(app(ty_@3, hh), baa), bab), eh, gd) → new_esEs1(zu31100, zu4500, hh, baa, bab)
new_esEs(Just(zu31100), Just(zu4500), app(app(ty_@2, bb), bc)) → new_esEs0(zu31100, zu4500, bb, bc)
new_esEs3(Right(zu31100), Right(zu4500), bdb, app(ty_[], bea)) → new_esEs2(zu31100, zu4500, bea)
new_esEs3(Left(zu31100), Left(zu4500), app(app(ty_@2, bcb), bcc), bca) → new_esEs0(zu31100, zu4500, bcb, bcc)
new_esEs2(:(zu31100, zu31101), :(zu4500, zu4501), app(ty_Maybe, bag)) → new_esEs(zu31100, zu4500, bag)
new_esEs3(Right(zu31100), Right(zu4500), bdb, app(app(ty_@2, bdd), bde)) → new_esEs0(zu31100, zu4500, bdd, bde)
new_esEs2(:(zu31100, zu31101), :(zu4500, zu4501), baf) → new_esEs2(zu31101, zu4501, baf)
new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), app(ty_Maybe, de), df) → new_esEs(zu31100, zu4500, de)
new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), cb, app(ty_Maybe, cc)) → new_esEs(zu31101, zu4501, cc)
new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), app(ty_[], ed), df) → new_esEs2(zu31100, zu4500, ed)
new_esEs(Just(zu31100), Just(zu4500), app(app(ty_Either, bh), ca)) → new_esEs3(zu31100, zu4500, bh, ca)
new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), app(app(ty_@2, dg), dh), df) → new_esEs0(zu31100, zu4500, dg, dh)
new_esEs2(:(zu31100, zu31101), :(zu4500, zu4501), app(ty_[], bbe)) → new_esEs2(zu31100, zu4500, bbe)
new_esEs3(Right(zu31100), Right(zu4500), bdb, app(ty_Maybe, bdc)) → new_esEs(zu31100, zu4500, bdc)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), app(ty_[], bac), eh, gd) → new_esEs2(zu31100, zu4500, bac)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), app(app(ty_Either, bad), bae), eh, gd) → new_esEs3(zu31100, zu4500, bad, bae)
new_esEs2(:(zu31100, zu31101), :(zu4500, zu4501), app(app(ty_Either, bbf), bbg)) → new_esEs3(zu31100, zu4500, bbf, bbg)
new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), app(app(app(ty_@3, ea), eb), ec), df) → new_esEs1(zu31100, zu4500, ea, eb, ec)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, app(app(ty_@2, ge), gf), gd) → new_esEs0(zu31101, zu4501, ge, gf)
new_esEs(Just(zu31100), Just(zu4500), app(ty_[], bg)) → new_esEs2(zu31100, zu4500, bg)
new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), cb, app(app(ty_@2, cd), ce)) → new_esEs0(zu31101, zu4501, cd, ce)
new_esEs3(Left(zu31100), Left(zu4500), app(ty_Maybe, bbh), bca) → new_esEs(zu31100, zu4500, bbh)
new_esEs3(Left(zu31100), Left(zu4500), app(ty_[], bcg), bca) → new_esEs2(zu31100, zu4500, bcg)
new_esEs(Just(zu31100), Just(zu4500), app(app(app(ty_@3, bd), be), bf)) → new_esEs1(zu31100, zu4500, bd, be, bf)
new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, eh, app(ty_Maybe, fa)) → new_esEs(zu31102, zu4502, fa)
new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), cb, app(ty_[], db)) → new_esEs2(zu31101, zu4501, db)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs(Just(zu31100), Just(zu4500), app(ty_[], bg)) → new_esEs2(zu31100, zu4500, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Just(zu31100), Just(zu4500), app(app(app(ty_@3, bd), be), bf)) → new_esEs1(zu31100, zu4500, bd, be, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(Just(zu31100), Just(zu4500), app(app(ty_@2, bb), bc)) → new_esEs0(zu31100, zu4500, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(:(zu31100, zu31101), :(zu4500, zu4501), app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs1(zu31100, zu4500, bbb, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(:(zu31100, zu31101), :(zu4500, zu4501), app(app(ty_@2, bah), bba)) → new_esEs0(zu31100, zu4500, bah, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Just(zu31100), Just(zu4500), app(app(ty_Either, bh), ca)) → new_esEs3(zu31100, zu4500, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Just(zu31100), Just(zu4500), app(ty_Maybe, ba)) → new_esEs(zu31100, zu4500, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(:(zu31100, zu31101), :(zu4500, zu4501), app(app(ty_Either, bbf), bbg)) → new_esEs3(zu31100, zu4500, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(:(zu31100, zu31101), :(zu4500, zu4501), app(ty_Maybe, bag)) → new_esEs(zu31100, zu4500, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), app(ty_[], ed), df) → new_esEs2(zu31100, zu4500, ed)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), cb, app(ty_[], db)) → new_esEs2(zu31101, zu4501, db)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), cb, app(app(app(ty_@3, cf), cg), da)) → new_esEs1(zu31101, zu4501, cf, cg, da)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), app(app(app(ty_@3, ea), eb), ec), df) → new_esEs1(zu31100, zu4500, ea, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), app(app(ty_@2, dg), dh), df) → new_esEs0(zu31100, zu4500, dg, dh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), cb, app(app(ty_@2, cd), ce)) → new_esEs0(zu31101, zu4501, cd, ce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), app(app(ty_Either, ee), ef), df) → new_esEs3(zu31100, zu4500, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), cb, app(app(ty_Either, dc), dd)) → new_esEs3(zu31101, zu4501, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), app(ty_Maybe, de), df) → new_esEs(zu31100, zu4500, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(@2(zu31100, zu31101), @2(zu4500, zu4501), cb, app(ty_Maybe, cc)) → new_esEs(zu31101, zu4501, cc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Right(zu31100), Right(zu4500), bdb, app(ty_[], bea)) → new_esEs2(zu31100, zu4500, bea)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Left(zu31100), Left(zu4500), app(ty_[], bcg), bca) → new_esEs2(zu31100, zu4500, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, eh, app(ty_[], fh)) → new_esEs2(zu31102, zu4502, fh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, app(ty_[], hb), gd) → new_esEs2(zu31101, zu4501, hb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), app(ty_[], bac), eh, gd) → new_esEs2(zu31100, zu4500, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(:(zu31100, zu31101), :(zu4500, zu4501), baf) → new_esEs2(zu31101, zu4501, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs2(:(zu31100, zu31101), :(zu4500, zu4501), app(ty_[], bbe)) → new_esEs2(zu31100, zu4500, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Right(zu31100), Right(zu4500), bdb, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs1(zu31100, zu4500, bdf, bdg, bdh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(Left(zu31100), Left(zu4500), app(app(app(ty_@3, bcd), bce), bcf), bca) → new_esEs1(zu31100, zu4500, bcd, bce, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, app(app(app(ty_@3, gg), gh), ha), gd) → new_esEs1(zu31101, zu4501, gg, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, eh, app(app(app(ty_@3, fd), ff), fg)) → new_esEs1(zu31102, zu4502, fd, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), app(app(app(ty_@3, hh), baa), bab), eh, gd) → new_esEs1(zu31100, zu4500, hh, baa, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Left(zu31100), Left(zu4500), app(app(ty_@2, bcb), bcc), bca) → new_esEs0(zu31100, zu4500, bcb, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Right(zu31100), Right(zu4500), bdb, app(app(ty_@2, bdd), bde)) → new_esEs0(zu31100, zu4500, bdd, bde)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(Right(zu31100), Right(zu4500), bdb, app(app(ty_Either, beb), bec)) → new_esEs3(zu31100, zu4500, beb, bec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(Left(zu31100), Left(zu4500), app(app(ty_Either, bch), bda), bca) → new_esEs3(zu31100, zu4500, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Right(zu31100), Right(zu4500), bdb, app(ty_Maybe, bdc)) → new_esEs(zu31100, zu4500, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(Left(zu31100), Left(zu4500), app(ty_Maybe, bbh), bca) → new_esEs(zu31100, zu4500, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, eh, app(app(ty_@2, fb), fc)) → new_esEs0(zu31102, zu4502, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), app(app(ty_@2, hf), hg), eh, gd) → new_esEs0(zu31100, zu4500, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, app(app(ty_@2, ge), gf), gd) → new_esEs0(zu31101, zu4501, ge, gf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, app(app(ty_Either, hc), hd), gd) → new_esEs3(zu31101, zu4501, hc, hd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, eh, app(app(ty_Either, ga), gb)) → new_esEs3(zu31102, zu4502, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), app(app(ty_Either, bad), bae), eh, gd) → new_esEs3(zu31100, zu4500, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, app(ty_Maybe, gc), gd) → new_esEs(zu31101, zu4501, gc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), app(ty_Maybe, he), eh, gd) → new_esEs(zu31100, zu4500, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), eg, eh, app(ty_Maybe, fa)) → new_esEs(zu31102, zu4502, fa)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_nubByNubBy'1(zu379, zu380, zu381, zu382, False, :(zu3840, zu3841), ba) → new_nubByNubBy'1(zu379, zu380, zu381, zu382, new_esEs4(zu3840, zu379, ba), zu3841, ba)
new_nubByNubBy'10(zu379, zu380, zu381, zu382, [], ba) → new_nubByNubBy'(zu380, zu379, :(zu381, zu382), ba)
new_nubByNubBy'1(zu379, :(zu3800, zu3801), zu381, zu382, True, zu384, ba) → new_nubByNubBy'10(zu3800, zu3801, zu381, zu382, :(zu381, zu382), ba)
new_nubByNubBy'1(zu379, zu380, zu381, zu382, False, [], ba) → new_nubByNubBy'(zu380, zu379, :(zu381, zu382), ba)
new_nubByNubBy'10(zu379, zu380, zu381, zu382, :(zu3840, zu3841), ba) → new_nubByNubBy'1(zu379, zu380, zu381, zu382, new_esEs4(zu3840, zu379, ba), zu3841, ba)
new_nubByNubBy'(:(zu3800, zu3801), zu381, zu382, ba) → new_nubByNubBy'10(zu3800, zu3801, zu381, zu382, :(zu381, zu382), ba)
The TRS R consists of the following rules:
new_esEs25(zu31100, zu4500, app(ty_[], bfd)) → new_esEs14(zu31100, zu4500, bfd)
new_esEs8(Just(zu31100), Just(zu4500), app(ty_[], bcf)) → new_esEs14(zu31100, zu4500, bcf)
new_esEs24(zu31101, zu4501, ty_@0) → new_esEs15(zu31101, zu4501)
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs26(zu31100, zu4500, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Char, ce) → new_esEs12(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(ty_Ratio, hh)) → new_esEs13(zu31101, zu4501, hh)
new_esEs8(Just(zu31100), Just(zu4500), ty_Bool) → new_esEs6(zu31100, zu4500)
new_primEqInt(Neg(Succ(zu311000)), Pos(zu4500)) → False
new_primEqInt(Pos(Succ(zu311000)), Neg(zu4500)) → False
new_esEs24(zu31101, zu4501, app(ty_Ratio, bea)) → new_esEs13(zu31101, zu4501, bea)
new_esEs23(zu31100, zu4500, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs4(zu3840, zu379, app(app(app(ty_@3, be), bf), bg)) → new_esEs10(zu3840, zu379, be, bf, bg)
new_esEs25(zu31100, zu4500, ty_Char) → new_esEs12(zu31100, zu4500)
new_esEs25(zu31100, zu4500, app(app(app(ty_@3, beh), bfa), bfb)) → new_esEs10(zu31100, zu4500, beh, bfa, bfb)
new_esEs26(zu31100, zu4500, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs24(zu31101, zu4501, ty_Ordering) → new_esEs11(zu31101, zu4501)
new_primEqInt(Pos(Zero), Neg(Succ(zu45000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(zu45000))) → False
new_esEs8(Just(zu31100), Just(zu4500), ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Float, ce) → new_esEs16(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Bool) → new_esEs6(zu31100, zu4500)
new_esEs4(zu3840, zu379, ty_Int) → new_esEs18(zu3840, zu379)
new_esEs21(zu31102, zu4502, ty_Ordering) → new_esEs11(zu31102, zu4502)
new_esEs23(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs22(zu31101, zu4501, ty_Char) → new_esEs12(zu31101, zu4501)
new_esEs24(zu31101, zu4501, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs10(zu31101, zu4501, bdf, bdg, bdh)
new_esEs11(EQ, EQ) → True
new_esEs23(zu31100, zu4500, ty_Float) → new_esEs16(zu31100, zu4500)
new_esEs8(Just(zu31100), Just(zu4500), ty_Float) → new_esEs16(zu31100, zu4500)
new_primMulNat0(Zero, Zero) → Zero
new_esEs17(Left(zu31100), Right(zu4500), ea, ce) → False
new_esEs17(Right(zu31100), Left(zu4500), ea, ce) → False
new_esEs26(zu31100, zu4500, ty_Float) → new_esEs16(zu31100, zu4500)
new_esEs12(Char(zu31100), Char(zu4500)) → new_primEqNat0(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(ty_Ratio, bbb)) → new_esEs13(zu31100, zu4500, bbb)
new_esEs8(Just(zu31100), Just(zu4500), ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs21(zu31102, zu4502, ty_Integer) → new_esEs5(zu31102, zu4502)
new_esEs23(zu31100, zu4500, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs11(GT, LT) → False
new_esEs11(LT, GT) → False
new_esEs25(zu31100, zu4500, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(app(app(ty_@3, bag), bah), bba)) → new_esEs10(zu31100, zu4500, bag, bah, bba)
new_esEs25(zu31100, zu4500, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs24(zu31101, zu4501, app(ty_[], beb)) → new_esEs14(zu31101, zu4501, beb)
new_esEs26(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(ty_Maybe, bad)) → new_esEs8(zu31100, zu4500, bad)
new_sr(Pos(zu311000), Neg(zu45000)) → Neg(new_primMulNat0(zu311000, zu45000))
new_sr(Neg(zu311000), Pos(zu45000)) → Neg(new_primMulNat0(zu311000, zu45000))
new_esEs11(EQ, LT) → False
new_esEs11(LT, EQ) → False
new_esEs19(zu31101, zu4501, ty_Int) → new_esEs18(zu31101, zu4501)
new_esEs20(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(app(ty_@2, bae), baf)) → new_esEs9(zu31100, zu4500, bae, baf)
new_esEs5(Integer(zu31100), Integer(zu4500)) → new_primEqInt(zu31100, zu4500)
new_esEs8(Just(zu31100), Just(zu4500), app(app(app(ty_@3, bcb), bcc), bcd)) → new_esEs10(zu31100, zu4500, bcb, bcc, bcd)
new_esEs4(zu3840, zu379, ty_Ordering) → new_esEs11(zu3840, zu379)
new_esEs26(zu31100, zu4500, ty_Bool) → new_esEs6(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(ty_[], baa)) → new_esEs14(zu31101, zu4501, baa)
new_primEqNat0(Succ(zu311000), Zero) → False
new_primEqNat0(Zero, Succ(zu45000)) → False
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Float) → new_esEs16(zu31100, zu4500)
new_primPlusNat0(Zero, Zero) → Zero
new_esEs4(zu3840, zu379, ty_Integer) → new_esEs5(zu3840, zu379)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs26(zu31100, zu4500, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs13(:%(zu31100, zu31101), :%(zu4500, zu4501), cd) → new_asAs(new_esEs20(zu31100, zu4500, cd), new_esEs19(zu31101, zu4501, cd))
new_esEs17(Right(zu31100), Right(zu4500), ea, app(ty_[], fa)) → new_esEs14(zu31100, zu4500, fa)
new_esEs14([], [], bfg) → True
new_esEs17(Left(zu31100), Left(zu4500), ty_Ordering, ce) → new_esEs11(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(app(app(ty_@3, he), hf), hg)) → new_esEs10(zu31101, zu4501, he, hf, hg)
new_esEs20(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs8(Just(zu31100), Just(zu4500), ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs21(zu31102, zu4502, ty_Double) → new_esEs7(zu31102, zu4502)
new_esEs21(zu31102, zu4502, app(app(ty_Either, gh), ha)) → new_esEs17(zu31102, zu4502, gh, ha)
new_esEs17(Left(zu31100), Left(zu4500), app(app(ty_Either, dg), dh), ce) → new_esEs17(zu31100, zu4500, dg, dh)
new_esEs26(zu31100, zu4500, ty_Char) → new_esEs12(zu31100, zu4500)
new_primPlusNat1(Succ(zu780), zu450000) → Succ(Succ(new_primPlusNat0(zu780, zu450000)))
new_esEs23(zu31100, zu4500, app(ty_[], bbc)) → new_esEs14(zu31100, zu4500, bbc)
new_esEs22(zu31101, zu4501, ty_@0) → new_esEs15(zu31101, zu4501)
new_esEs16(Float(zu31100, zu31101), Float(zu4500, zu4501)) → new_esEs18(new_sr(zu31100, zu4500), new_sr(zu31101, zu4501))
new_esEs8(Just(zu31100), Just(zu4500), ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs23(zu31100, zu4500, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs22(zu31101, zu4501, ty_Bool) → new_esEs6(zu31101, zu4501)
new_esEs21(zu31102, zu4502, ty_Int) → new_esEs18(zu31102, zu4502)
new_esEs6(True, True) → True
new_esEs25(zu31100, zu4500, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs18(zu3110, zu450) → new_primEqInt(zu3110, zu450)
new_esEs24(zu31101, zu4501, ty_Bool) → new_esEs6(zu31101, zu4501)
new_esEs17(Left(zu31100), Left(zu4500), app(ty_[], df), ce) → new_esEs14(zu31100, zu4500, df)
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Integer, ce) → new_esEs5(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), app(ty_Maybe, cf), ce) → new_esEs8(zu31100, zu4500, cf)
new_esEs22(zu31101, zu4501, ty_Double) → new_esEs7(zu31101, zu4501)
new_esEs8(Nothing, Nothing, bbf) → True
new_esEs21(zu31102, zu4502, app(ty_Ratio, gf)) → new_esEs13(zu31102, zu4502, gf)
new_esEs4(zu3840, zu379, ty_Char) → new_esEs12(zu3840, zu379)
new_esEs21(zu31102, zu4502, app(app(ty_@2, ga), gb)) → new_esEs9(zu31102, zu4502, ga, gb)
new_esEs4(zu3840, zu379, app(ty_Maybe, bb)) → new_esEs8(zu3840, zu379, bb)
new_esEs11(GT, GT) → True
new_esEs17(Right(zu31100), Right(zu4500), ea, app(app(ty_@2, ec), ed)) → new_esEs9(zu31100, zu4500, ec, ed)
new_sr(Neg(zu311000), Neg(zu45000)) → Pos(new_primMulNat0(zu311000, zu45000))
new_esEs15(@0, @0) → True
new_esEs24(zu31101, zu4501, app(app(ty_Either, bec), bed)) → new_esEs17(zu31101, zu4501, bec, bed)
new_esEs10(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), fd, ff, fg) → new_asAs(new_esEs23(zu31100, zu4500, fd), new_asAs(new_esEs22(zu31101, zu4501, ff), new_esEs21(zu31102, zu4502, fg)))
new_esEs22(zu31101, zu4501, app(app(ty_@2, hc), hd)) → new_esEs9(zu31101, zu4501, hc, hd)
new_esEs25(zu31100, zu4500, app(ty_Ratio, bfc)) → new_esEs13(zu31100, zu4500, bfc)
new_esEs25(zu31100, zu4500, app(app(ty_Either, bfe), bff)) → new_esEs17(zu31100, zu4500, bfe, bff)
new_sr(Pos(zu311000), Pos(zu45000)) → Pos(new_primMulNat0(zu311000, zu45000))
new_asAs(False, zu68) → False
new_esEs8(Just(zu31100), Just(zu4500), ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs22(zu31101, zu4501, ty_Int) → new_esEs18(zu31101, zu4501)
new_primEqNat0(Zero, Zero) → True
new_esEs17(Left(zu31100), Left(zu4500), ty_Bool, ce) → new_esEs6(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(ty_Maybe, hb)) → new_esEs8(zu31101, zu4501, hb)
new_primMulNat0(Zero, Succ(zu450000)) → Zero
new_primMulNat0(Succ(zu3110000), Zero) → Zero
new_esEs21(zu31102, zu4502, ty_Bool) → new_esEs6(zu31102, zu4502)
new_primMulNat0(Succ(zu3110000), Succ(zu450000)) → new_primPlusNat1(new_primMulNat0(zu3110000, Succ(zu450000)), zu450000)
new_esEs26(zu31100, zu4500, app(app(ty_@2, bga), bgb)) → new_esEs9(zu31100, zu4500, bga, bgb)
new_esEs26(zu31100, zu4500, app(ty_Ratio, bgf)) → new_esEs13(zu31100, zu4500, bgf)
new_esEs24(zu31101, zu4501, ty_Integer) → new_esEs5(zu31101, zu4501)
new_esEs22(zu31101, zu4501, ty_Integer) → new_esEs5(zu31101, zu4501)
new_esEs23(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), app(app(app(ty_@3, db), dc), dd), ce) → new_esEs10(zu31100, zu4500, db, dc, dd)
new_esEs4(zu3840, zu379, ty_Bool) → new_esEs6(zu3840, zu379)
new_esEs21(zu31102, zu4502, app(ty_Maybe, fh)) → new_esEs8(zu31102, zu4502, fh)
new_esEs23(zu31100, zu4500, ty_Char) → new_esEs12(zu31100, zu4500)
new_esEs4(zu3840, zu379, app(ty_[], ca)) → new_esEs14(zu3840, zu379, ca)
new_esEs17(Left(zu31100), Left(zu4500), ty_Int, ce) → new_esEs18(zu31100, zu4500)
new_esEs24(zu31101, zu4501, ty_Char) → new_esEs12(zu31101, zu4501)
new_esEs26(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs25(zu31100, zu4500, ty_Float) → new_esEs16(zu31100, zu4500)
new_esEs25(zu31100, zu4500, app(app(ty_@2, bef), beg)) → new_esEs9(zu31100, zu4500, bef, beg)
new_esEs8(Just(zu31100), Nothing, bbf) → False
new_esEs8(Nothing, Just(zu4500), bbf) → False
new_esEs22(zu31101, zu4501, ty_Float) → new_esEs16(zu31101, zu4501)
new_esEs24(zu31101, zu4501, ty_Double) → new_esEs7(zu31101, zu4501)
new_esEs4(zu3840, zu379, ty_@0) → new_esEs15(zu3840, zu379)
new_primEqInt(Neg(Succ(zu311000)), Neg(Succ(zu45000))) → new_primEqNat0(zu311000, zu45000)
new_esEs17(Right(zu31100), Right(zu4500), ea, app(app(app(ty_@3, ee), ef), eg)) → new_esEs10(zu31100, zu4500, ee, ef, eg)
new_esEs19(zu31101, zu4501, ty_Integer) → new_esEs5(zu31101, zu4501)
new_esEs26(zu31100, zu4500, app(ty_Maybe, bfh)) → new_esEs8(zu31100, zu4500, bfh)
new_esEs8(Just(zu31100), Just(zu4500), app(app(ty_@2, bbh), bca)) → new_esEs9(zu31100, zu4500, bbh, bca)
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), ea, app(app(ty_Either, fb), fc)) → new_esEs17(zu31100, zu4500, fb, fc)
new_esEs8(Just(zu31100), Just(zu4500), app(ty_Ratio, bce)) → new_esEs13(zu31100, zu4500, bce)
new_esEs23(zu31100, zu4500, app(app(ty_Either, bbd), bbe)) → new_esEs17(zu31100, zu4500, bbd, bbe)
new_esEs21(zu31102, zu4502, ty_Char) → new_esEs12(zu31102, zu4502)
new_esEs26(zu31100, zu4500, app(app(ty_Either, bgh), bha)) → new_esEs17(zu31100, zu4500, bgh, bha)
new_esEs24(zu31101, zu4501, app(ty_Maybe, bdc)) → new_esEs8(zu31101, zu4501, bdc)
new_esEs21(zu31102, zu4502, ty_@0) → new_esEs15(zu31102, zu4502)
new_esEs14(:(zu31100, zu31101), [], bfg) → False
new_esEs14([], :(zu4500, zu4501), bfg) → False
new_esEs25(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs8(Just(zu31100), Just(zu4500), ty_Char) → new_esEs12(zu31100, zu4500)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs4(zu3840, zu379, ty_Float) → new_esEs16(zu3840, zu379)
new_esEs26(zu31100, zu4500, app(ty_[], bgg)) → new_esEs14(zu31100, zu4500, bgg)
new_esEs17(Left(zu31100), Left(zu4500), app(app(ty_@2, cg), da), ce) → new_esEs9(zu31100, zu4500, cg, da)
new_primEqInt(Neg(Succ(zu311000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(zu45000))) → False
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Char) → new_esEs12(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), ea, app(ty_Maybe, eb)) → new_esEs8(zu31100, zu4500, eb)
new_esEs24(zu31101, zu4501, app(app(ty_@2, bdd), bde)) → new_esEs9(zu31101, zu4501, bdd, bde)
new_primPlusNat1(Zero, zu450000) → Succ(zu450000)
new_primPlusNat0(Succ(zu7800), Succ(zu4500000)) → Succ(Succ(new_primPlusNat0(zu7800, zu4500000)))
new_esEs21(zu31102, zu4502, app(app(app(ty_@3, gc), gd), ge)) → new_esEs10(zu31102, zu4502, gc, gd, ge)
new_esEs17(Left(zu31100), Left(zu4500), ty_Double, ce) → new_esEs7(zu31100, zu4500)
new_esEs7(Double(zu31100, zu31101), Double(zu4500, zu4501)) → new_esEs18(new_sr(zu31100, zu4500), new_sr(zu31101, zu4501))
new_esEs4(zu3840, zu379, app(app(ty_Either, cb), cc)) → new_esEs17(zu3840, zu379, cb, cc)
new_esEs14(:(zu31100, zu31101), :(zu4500, zu4501), bfg) → new_asAs(new_esEs26(zu31100, zu4500, bfg), new_esEs14(zu31101, zu4501, bfg))
new_esEs24(zu31101, zu4501, ty_Float) → new_esEs16(zu31101, zu4501)
new_asAs(True, zu68) → zu68
new_esEs11(LT, LT) → True
new_esEs4(zu3840, zu379, app(app(ty_@2, bc), bd)) → new_esEs9(zu3840, zu379, bc, bd)
new_esEs8(Just(zu31100), Just(zu4500), app(ty_Maybe, bbg)) → new_esEs8(zu31100, zu4500, bbg)
new_esEs23(zu31100, zu4500, ty_Bool) → new_esEs6(zu31100, zu4500)
new_primEqInt(Pos(Succ(zu311000)), Pos(Succ(zu45000))) → new_primEqNat0(zu311000, zu45000)
new_esEs25(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs6(True, False) → False
new_esEs6(False, True) → False
new_esEs8(Just(zu31100), Just(zu4500), app(app(ty_Either, bcg), bch)) → new_esEs17(zu31100, zu4500, bcg, bch)
new_esEs24(zu31101, zu4501, ty_Int) → new_esEs18(zu31101, zu4501)
new_esEs6(False, False) → True
new_esEs9(@2(zu31100, zu31101), @2(zu4500, zu4501), bda, bdb) → new_asAs(new_esEs25(zu31100, zu4500, bda), new_esEs24(zu31101, zu4501, bdb))
new_primEqNat0(Succ(zu311000), Succ(zu45000)) → new_primEqNat0(zu311000, zu45000)
new_esEs11(GT, EQ) → False
new_esEs11(EQ, GT) → False
new_esEs17(Left(zu31100), Left(zu4500), app(ty_Ratio, de), ce) → new_esEs13(zu31100, zu4500, de)
new_esEs21(zu31102, zu4502, app(ty_[], gg)) → new_esEs14(zu31102, zu4502, gg)
new_esEs25(zu31100, zu4500, ty_Bool) → new_esEs6(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), ea, app(ty_Ratio, eh)) → new_esEs13(zu31100, zu4500, eh)
new_esEs21(zu31102, zu4502, ty_Float) → new_esEs16(zu31102, zu4502)
new_esEs25(zu31100, zu4500, app(ty_Maybe, bee)) → new_esEs8(zu31100, zu4500, bee)
new_esEs17(Left(zu31100), Left(zu4500), ty_@0, ce) → new_esEs15(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_primEqInt(Pos(Zero), Pos(Succ(zu45000))) → False
new_primEqInt(Pos(Succ(zu311000)), Pos(Zero)) → False
new_esEs4(zu3840, zu379, app(ty_Ratio, bh)) → new_esEs13(zu3840, zu379, bh)
new_esEs22(zu31101, zu4501, ty_Ordering) → new_esEs11(zu31101, zu4501)
new_esEs22(zu31101, zu4501, app(app(ty_Either, bab), bac)) → new_esEs17(zu31101, zu4501, bab, bac)
new_esEs26(zu31100, zu4500, app(app(app(ty_@3, bgc), bgd), bge)) → new_esEs10(zu31100, zu4500, bgc, bgd, bge)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primPlusNat0(Succ(zu7800), Zero) → Succ(zu7800)
new_primPlusNat0(Zero, Succ(zu4500000)) → Succ(zu4500000)
new_esEs4(zu3840, zu379, ty_Double) → new_esEs7(zu3840, zu379)
The set Q consists of the following terms:
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Int)
new_esEs8(Just(x0), Just(x1), ty_Bool)
new_esEs22(x0, x1, ty_Double)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(Left(x0), Left(x1), ty_Int, x2)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Integer)
new_esEs13(:%(x0, x1), :%(x2, x3), x4)
new_esEs21(x0, x1, ty_Char)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs17(Left(x0), Left(x1), ty_Char, x2)
new_esEs10(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs11(EQ, LT)
new_esEs11(LT, EQ)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs8(Just(x0), Just(x1), ty_Double)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Zero, Succ(x0))
new_esEs26(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Right(x0), Right(x1), x2, ty_Bool)
new_esEs24(x0, x1, ty_Int)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs17(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs9(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs14(:(x0, x1), [], x2)
new_esEs23(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Char)
new_primPlusNat1(Zero, x0)
new_esEs4(x0, x1, ty_@0)
new_esEs20(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_asAs(True, x0)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(False, x0)
new_esEs24(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Integer)
new_sr(Pos(x0), Pos(x1))
new_esEs23(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs18(x0, x1)
new_esEs12(Char(x0), Char(x1))
new_esEs23(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Bool)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_primEqNat0(Succ(x0), Zero)
new_esEs11(EQ, GT)
new_esEs11(GT, EQ)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, ty_Integer)
new_esEs8(Nothing, Just(x0), x1)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs22(x0, x1, ty_Char)
new_esEs8(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primEqNat0(Zero, Zero)
new_primEqNat0(Zero, Succ(x0))
new_esEs17(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs15(@0, @0)
new_esEs21(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Ordering)
new_esEs17(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs6(False, False)
new_esEs4(x0, x1, ty_Integer)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Left(x0), Left(x1), ty_Float, x2)
new_esEs21(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Ordering)
new_esEs23(x0, x1, ty_Ordering)
new_esEs8(Just(x0), Just(x1), ty_Int)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(Integer(x0), Integer(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Bool)
new_esEs14([], [], x0)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs25(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs17(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Ordering)
new_esEs17(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs26(x0, x1, ty_Integer)
new_esEs11(GT, GT)
new_esEs19(x0, x1, ty_Integer)
new_esEs16(Float(x0, x1), Float(x2, x3))
new_esEs8(Just(x0), Just(x1), ty_@0)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Right(x0), Right(x1), x2, ty_Float)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_@0)
new_esEs8(Just(x0), Just(x1), ty_Ordering)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs11(LT, GT)
new_esEs11(GT, LT)
new_esEs25(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Char)
new_primMulNat0(Succ(x0), Zero)
new_esEs19(x0, x1, ty_Int)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs17(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Left(x0), Left(x1), ty_Integer, x2)
new_esEs26(x0, x1, ty_Bool)
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs17(Right(x0), Left(x1), x2, x3)
new_esEs17(Left(x0), Right(x1), x2, x3)
new_esEs4(x0, x1, ty_Float)
new_primPlusNat0(Succ(x0), Zero)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs17(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs17(Right(x0), Right(x1), x2, ty_@0)
new_esEs8(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_@0)
new_primPlusNat1(Succ(x0), x1)
new_esEs17(Right(x0), Right(x1), x2, ty_Int)
new_esEs21(x0, x1, ty_Ordering)
new_esEs17(Right(x0), Right(x1), x2, ty_Integer)
new_esEs21(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Double)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_sr(Neg(x0), Neg(x1))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs17(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs11(LT, LT)
new_esEs22(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs23(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Float)
new_primPlusNat0(Zero, Zero)
new_esEs8(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Nothing, Nothing, x0)
new_esEs8(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs6(True, True)
new_esEs8(Just(x0), Just(x1), ty_Float)
new_esEs4(x0, x1, ty_Char)
new_esEs14([], :(x0, x1), x2)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs21(x0, x1, ty_Int)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs17(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs11(EQ, EQ)
new_esEs8(Just(x0), Just(x1), app(ty_[], x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs6(False, True)
new_esEs6(True, False)
new_esEs4(x0, x1, ty_Int)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs8(Just(x0), Just(x1), ty_Char)
new_esEs17(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs17(Left(x0), Left(x1), ty_Double, x2)
new_esEs23(x0, x1, ty_Integer)
new_esEs8(Just(x0), Nothing, x1)
new_esEs17(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs23(x0, x1, ty_Bool)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(Double(x0, x1), Double(x2, x3))
new_esEs17(Right(x0), Right(x1), x2, ty_Char)
new_esEs25(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, ty_Bool)
new_esEs8(Just(x0), Just(x1), ty_Integer)
new_esEs17(Right(x0), Right(x1), x2, ty_Double)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs17(Left(x0), Left(x1), ty_@0, x2)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_nubByNubBy'1(zu379, zu380, zu381, zu382, False, :(zu3840, zu3841), ba) → new_nubByNubBy'1(zu379, zu380, zu381, zu382, new_esEs4(zu3840, zu379, ba), zu3841, ba)
new_nubByNubBy'1(zu379, :(zu3800, zu3801), zu381, zu382, True, zu384, ba) → new_nubByNubBy'10(zu3800, zu3801, zu381, zu382, :(zu381, zu382), ba)
new_nubByNubBy'1(zu379, zu380, zu381, zu382, False, [], ba) → new_nubByNubBy'(zu380, zu379, :(zu381, zu382), ba)
new_nubByNubBy'10(zu379, zu380, zu381, zu382, :(zu3840, zu3841), ba) → new_nubByNubBy'1(zu379, zu380, zu381, zu382, new_esEs4(zu3840, zu379, ba), zu3841, ba)
new_nubByNubBy'(:(zu3800, zu3801), zu381, zu382, ba) → new_nubByNubBy'10(zu3800, zu3801, zu381, zu382, :(zu381, zu382), ba)
The TRS R consists of the following rules:
new_esEs25(zu31100, zu4500, app(ty_[], bfd)) → new_esEs14(zu31100, zu4500, bfd)
new_esEs8(Just(zu31100), Just(zu4500), app(ty_[], bcf)) → new_esEs14(zu31100, zu4500, bcf)
new_esEs24(zu31101, zu4501, ty_@0) → new_esEs15(zu31101, zu4501)
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs26(zu31100, zu4500, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Char, ce) → new_esEs12(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(ty_Ratio, hh)) → new_esEs13(zu31101, zu4501, hh)
new_esEs8(Just(zu31100), Just(zu4500), ty_Bool) → new_esEs6(zu31100, zu4500)
new_primEqInt(Neg(Succ(zu311000)), Pos(zu4500)) → False
new_primEqInt(Pos(Succ(zu311000)), Neg(zu4500)) → False
new_esEs24(zu31101, zu4501, app(ty_Ratio, bea)) → new_esEs13(zu31101, zu4501, bea)
new_esEs23(zu31100, zu4500, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs4(zu3840, zu379, app(app(app(ty_@3, be), bf), bg)) → new_esEs10(zu3840, zu379, be, bf, bg)
new_esEs25(zu31100, zu4500, ty_Char) → new_esEs12(zu31100, zu4500)
new_esEs25(zu31100, zu4500, app(app(app(ty_@3, beh), bfa), bfb)) → new_esEs10(zu31100, zu4500, beh, bfa, bfb)
new_esEs26(zu31100, zu4500, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs24(zu31101, zu4501, ty_Ordering) → new_esEs11(zu31101, zu4501)
new_primEqInt(Pos(Zero), Neg(Succ(zu45000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(zu45000))) → False
new_esEs8(Just(zu31100), Just(zu4500), ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Float, ce) → new_esEs16(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Bool) → new_esEs6(zu31100, zu4500)
new_esEs4(zu3840, zu379, ty_Int) → new_esEs18(zu3840, zu379)
new_esEs21(zu31102, zu4502, ty_Ordering) → new_esEs11(zu31102, zu4502)
new_esEs23(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs22(zu31101, zu4501, ty_Char) → new_esEs12(zu31101, zu4501)
new_esEs24(zu31101, zu4501, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs10(zu31101, zu4501, bdf, bdg, bdh)
new_esEs11(EQ, EQ) → True
new_esEs23(zu31100, zu4500, ty_Float) → new_esEs16(zu31100, zu4500)
new_esEs8(Just(zu31100), Just(zu4500), ty_Float) → new_esEs16(zu31100, zu4500)
new_primMulNat0(Zero, Zero) → Zero
new_esEs17(Left(zu31100), Right(zu4500), ea, ce) → False
new_esEs17(Right(zu31100), Left(zu4500), ea, ce) → False
new_esEs26(zu31100, zu4500, ty_Float) → new_esEs16(zu31100, zu4500)
new_esEs12(Char(zu31100), Char(zu4500)) → new_primEqNat0(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(ty_Ratio, bbb)) → new_esEs13(zu31100, zu4500, bbb)
new_esEs8(Just(zu31100), Just(zu4500), ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs21(zu31102, zu4502, ty_Integer) → new_esEs5(zu31102, zu4502)
new_esEs23(zu31100, zu4500, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs11(GT, LT) → False
new_esEs11(LT, GT) → False
new_esEs25(zu31100, zu4500, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(app(app(ty_@3, bag), bah), bba)) → new_esEs10(zu31100, zu4500, bag, bah, bba)
new_esEs25(zu31100, zu4500, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs24(zu31101, zu4501, app(ty_[], beb)) → new_esEs14(zu31101, zu4501, beb)
new_esEs26(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(ty_Maybe, bad)) → new_esEs8(zu31100, zu4500, bad)
new_sr(Pos(zu311000), Neg(zu45000)) → Neg(new_primMulNat0(zu311000, zu45000))
new_sr(Neg(zu311000), Pos(zu45000)) → Neg(new_primMulNat0(zu311000, zu45000))
new_esEs11(EQ, LT) → False
new_esEs11(LT, EQ) → False
new_esEs19(zu31101, zu4501, ty_Int) → new_esEs18(zu31101, zu4501)
new_esEs20(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(app(ty_@2, bae), baf)) → new_esEs9(zu31100, zu4500, bae, baf)
new_esEs5(Integer(zu31100), Integer(zu4500)) → new_primEqInt(zu31100, zu4500)
new_esEs8(Just(zu31100), Just(zu4500), app(app(app(ty_@3, bcb), bcc), bcd)) → new_esEs10(zu31100, zu4500, bcb, bcc, bcd)
new_esEs4(zu3840, zu379, ty_Ordering) → new_esEs11(zu3840, zu379)
new_esEs26(zu31100, zu4500, ty_Bool) → new_esEs6(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(ty_[], baa)) → new_esEs14(zu31101, zu4501, baa)
new_primEqNat0(Succ(zu311000), Zero) → False
new_primEqNat0(Zero, Succ(zu45000)) → False
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Float) → new_esEs16(zu31100, zu4500)
new_primPlusNat0(Zero, Zero) → Zero
new_esEs4(zu3840, zu379, ty_Integer) → new_esEs5(zu3840, zu379)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs26(zu31100, zu4500, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs13(:%(zu31100, zu31101), :%(zu4500, zu4501), cd) → new_asAs(new_esEs20(zu31100, zu4500, cd), new_esEs19(zu31101, zu4501, cd))
new_esEs17(Right(zu31100), Right(zu4500), ea, app(ty_[], fa)) → new_esEs14(zu31100, zu4500, fa)
new_esEs14([], [], bfg) → True
new_esEs17(Left(zu31100), Left(zu4500), ty_Ordering, ce) → new_esEs11(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(app(app(ty_@3, he), hf), hg)) → new_esEs10(zu31101, zu4501, he, hf, hg)
new_esEs20(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs8(Just(zu31100), Just(zu4500), ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs21(zu31102, zu4502, ty_Double) → new_esEs7(zu31102, zu4502)
new_esEs21(zu31102, zu4502, app(app(ty_Either, gh), ha)) → new_esEs17(zu31102, zu4502, gh, ha)
new_esEs17(Left(zu31100), Left(zu4500), app(app(ty_Either, dg), dh), ce) → new_esEs17(zu31100, zu4500, dg, dh)
new_esEs26(zu31100, zu4500, ty_Char) → new_esEs12(zu31100, zu4500)
new_primPlusNat1(Succ(zu780), zu450000) → Succ(Succ(new_primPlusNat0(zu780, zu450000)))
new_esEs23(zu31100, zu4500, app(ty_[], bbc)) → new_esEs14(zu31100, zu4500, bbc)
new_esEs22(zu31101, zu4501, ty_@0) → new_esEs15(zu31101, zu4501)
new_esEs16(Float(zu31100, zu31101), Float(zu4500, zu4501)) → new_esEs18(new_sr(zu31100, zu4500), new_sr(zu31101, zu4501))
new_esEs8(Just(zu31100), Just(zu4500), ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs23(zu31100, zu4500, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs22(zu31101, zu4501, ty_Bool) → new_esEs6(zu31101, zu4501)
new_esEs21(zu31102, zu4502, ty_Int) → new_esEs18(zu31102, zu4502)
new_esEs6(True, True) → True
new_esEs25(zu31100, zu4500, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs18(zu3110, zu450) → new_primEqInt(zu3110, zu450)
new_esEs24(zu31101, zu4501, ty_Bool) → new_esEs6(zu31101, zu4501)
new_esEs17(Left(zu31100), Left(zu4500), app(ty_[], df), ce) → new_esEs14(zu31100, zu4500, df)
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Integer, ce) → new_esEs5(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), app(ty_Maybe, cf), ce) → new_esEs8(zu31100, zu4500, cf)
new_esEs22(zu31101, zu4501, ty_Double) → new_esEs7(zu31101, zu4501)
new_esEs8(Nothing, Nothing, bbf) → True
new_esEs21(zu31102, zu4502, app(ty_Ratio, gf)) → new_esEs13(zu31102, zu4502, gf)
new_esEs4(zu3840, zu379, ty_Char) → new_esEs12(zu3840, zu379)
new_esEs21(zu31102, zu4502, app(app(ty_@2, ga), gb)) → new_esEs9(zu31102, zu4502, ga, gb)
new_esEs4(zu3840, zu379, app(ty_Maybe, bb)) → new_esEs8(zu3840, zu379, bb)
new_esEs11(GT, GT) → True
new_esEs17(Right(zu31100), Right(zu4500), ea, app(app(ty_@2, ec), ed)) → new_esEs9(zu31100, zu4500, ec, ed)
new_sr(Neg(zu311000), Neg(zu45000)) → Pos(new_primMulNat0(zu311000, zu45000))
new_esEs15(@0, @0) → True
new_esEs24(zu31101, zu4501, app(app(ty_Either, bec), bed)) → new_esEs17(zu31101, zu4501, bec, bed)
new_esEs10(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), fd, ff, fg) → new_asAs(new_esEs23(zu31100, zu4500, fd), new_asAs(new_esEs22(zu31101, zu4501, ff), new_esEs21(zu31102, zu4502, fg)))
new_esEs22(zu31101, zu4501, app(app(ty_@2, hc), hd)) → new_esEs9(zu31101, zu4501, hc, hd)
new_esEs25(zu31100, zu4500, app(ty_Ratio, bfc)) → new_esEs13(zu31100, zu4500, bfc)
new_esEs25(zu31100, zu4500, app(app(ty_Either, bfe), bff)) → new_esEs17(zu31100, zu4500, bfe, bff)
new_sr(Pos(zu311000), Pos(zu45000)) → Pos(new_primMulNat0(zu311000, zu45000))
new_asAs(False, zu68) → False
new_esEs8(Just(zu31100), Just(zu4500), ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs22(zu31101, zu4501, ty_Int) → new_esEs18(zu31101, zu4501)
new_primEqNat0(Zero, Zero) → True
new_esEs17(Left(zu31100), Left(zu4500), ty_Bool, ce) → new_esEs6(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(ty_Maybe, hb)) → new_esEs8(zu31101, zu4501, hb)
new_primMulNat0(Zero, Succ(zu450000)) → Zero
new_primMulNat0(Succ(zu3110000), Zero) → Zero
new_esEs21(zu31102, zu4502, ty_Bool) → new_esEs6(zu31102, zu4502)
new_primMulNat0(Succ(zu3110000), Succ(zu450000)) → new_primPlusNat1(new_primMulNat0(zu3110000, Succ(zu450000)), zu450000)
new_esEs26(zu31100, zu4500, app(app(ty_@2, bga), bgb)) → new_esEs9(zu31100, zu4500, bga, bgb)
new_esEs26(zu31100, zu4500, app(ty_Ratio, bgf)) → new_esEs13(zu31100, zu4500, bgf)
new_esEs24(zu31101, zu4501, ty_Integer) → new_esEs5(zu31101, zu4501)
new_esEs22(zu31101, zu4501, ty_Integer) → new_esEs5(zu31101, zu4501)
new_esEs23(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), app(app(app(ty_@3, db), dc), dd), ce) → new_esEs10(zu31100, zu4500, db, dc, dd)
new_esEs4(zu3840, zu379, ty_Bool) → new_esEs6(zu3840, zu379)
new_esEs21(zu31102, zu4502, app(ty_Maybe, fh)) → new_esEs8(zu31102, zu4502, fh)
new_esEs23(zu31100, zu4500, ty_Char) → new_esEs12(zu31100, zu4500)
new_esEs4(zu3840, zu379, app(ty_[], ca)) → new_esEs14(zu3840, zu379, ca)
new_esEs17(Left(zu31100), Left(zu4500), ty_Int, ce) → new_esEs18(zu31100, zu4500)
new_esEs24(zu31101, zu4501, ty_Char) → new_esEs12(zu31101, zu4501)
new_esEs26(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs25(zu31100, zu4500, ty_Float) → new_esEs16(zu31100, zu4500)
new_esEs25(zu31100, zu4500, app(app(ty_@2, bef), beg)) → new_esEs9(zu31100, zu4500, bef, beg)
new_esEs8(Just(zu31100), Nothing, bbf) → False
new_esEs8(Nothing, Just(zu4500), bbf) → False
new_esEs22(zu31101, zu4501, ty_Float) → new_esEs16(zu31101, zu4501)
new_esEs24(zu31101, zu4501, ty_Double) → new_esEs7(zu31101, zu4501)
new_esEs4(zu3840, zu379, ty_@0) → new_esEs15(zu3840, zu379)
new_primEqInt(Neg(Succ(zu311000)), Neg(Succ(zu45000))) → new_primEqNat0(zu311000, zu45000)
new_esEs17(Right(zu31100), Right(zu4500), ea, app(app(app(ty_@3, ee), ef), eg)) → new_esEs10(zu31100, zu4500, ee, ef, eg)
new_esEs19(zu31101, zu4501, ty_Integer) → new_esEs5(zu31101, zu4501)
new_esEs26(zu31100, zu4500, app(ty_Maybe, bfh)) → new_esEs8(zu31100, zu4500, bfh)
new_esEs8(Just(zu31100), Just(zu4500), app(app(ty_@2, bbh), bca)) → new_esEs9(zu31100, zu4500, bbh, bca)
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), ea, app(app(ty_Either, fb), fc)) → new_esEs17(zu31100, zu4500, fb, fc)
new_esEs8(Just(zu31100), Just(zu4500), app(ty_Ratio, bce)) → new_esEs13(zu31100, zu4500, bce)
new_esEs23(zu31100, zu4500, app(app(ty_Either, bbd), bbe)) → new_esEs17(zu31100, zu4500, bbd, bbe)
new_esEs21(zu31102, zu4502, ty_Char) → new_esEs12(zu31102, zu4502)
new_esEs26(zu31100, zu4500, app(app(ty_Either, bgh), bha)) → new_esEs17(zu31100, zu4500, bgh, bha)
new_esEs24(zu31101, zu4501, app(ty_Maybe, bdc)) → new_esEs8(zu31101, zu4501, bdc)
new_esEs21(zu31102, zu4502, ty_@0) → new_esEs15(zu31102, zu4502)
new_esEs14(:(zu31100, zu31101), [], bfg) → False
new_esEs14([], :(zu4500, zu4501), bfg) → False
new_esEs25(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs8(Just(zu31100), Just(zu4500), ty_Char) → new_esEs12(zu31100, zu4500)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs4(zu3840, zu379, ty_Float) → new_esEs16(zu3840, zu379)
new_esEs26(zu31100, zu4500, app(ty_[], bgg)) → new_esEs14(zu31100, zu4500, bgg)
new_esEs17(Left(zu31100), Left(zu4500), app(app(ty_@2, cg), da), ce) → new_esEs9(zu31100, zu4500, cg, da)
new_primEqInt(Neg(Succ(zu311000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(zu45000))) → False
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Char) → new_esEs12(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), ea, app(ty_Maybe, eb)) → new_esEs8(zu31100, zu4500, eb)
new_esEs24(zu31101, zu4501, app(app(ty_@2, bdd), bde)) → new_esEs9(zu31101, zu4501, bdd, bde)
new_primPlusNat1(Zero, zu450000) → Succ(zu450000)
new_primPlusNat0(Succ(zu7800), Succ(zu4500000)) → Succ(Succ(new_primPlusNat0(zu7800, zu4500000)))
new_esEs21(zu31102, zu4502, app(app(app(ty_@3, gc), gd), ge)) → new_esEs10(zu31102, zu4502, gc, gd, ge)
new_esEs17(Left(zu31100), Left(zu4500), ty_Double, ce) → new_esEs7(zu31100, zu4500)
new_esEs7(Double(zu31100, zu31101), Double(zu4500, zu4501)) → new_esEs18(new_sr(zu31100, zu4500), new_sr(zu31101, zu4501))
new_esEs4(zu3840, zu379, app(app(ty_Either, cb), cc)) → new_esEs17(zu3840, zu379, cb, cc)
new_esEs14(:(zu31100, zu31101), :(zu4500, zu4501), bfg) → new_asAs(new_esEs26(zu31100, zu4500, bfg), new_esEs14(zu31101, zu4501, bfg))
new_esEs24(zu31101, zu4501, ty_Float) → new_esEs16(zu31101, zu4501)
new_asAs(True, zu68) → zu68
new_esEs11(LT, LT) → True
new_esEs4(zu3840, zu379, app(app(ty_@2, bc), bd)) → new_esEs9(zu3840, zu379, bc, bd)
new_esEs8(Just(zu31100), Just(zu4500), app(ty_Maybe, bbg)) → new_esEs8(zu31100, zu4500, bbg)
new_esEs23(zu31100, zu4500, ty_Bool) → new_esEs6(zu31100, zu4500)
new_primEqInt(Pos(Succ(zu311000)), Pos(Succ(zu45000))) → new_primEqNat0(zu311000, zu45000)
new_esEs25(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs6(True, False) → False
new_esEs6(False, True) → False
new_esEs8(Just(zu31100), Just(zu4500), app(app(ty_Either, bcg), bch)) → new_esEs17(zu31100, zu4500, bcg, bch)
new_esEs24(zu31101, zu4501, ty_Int) → new_esEs18(zu31101, zu4501)
new_esEs6(False, False) → True
new_esEs9(@2(zu31100, zu31101), @2(zu4500, zu4501), bda, bdb) → new_asAs(new_esEs25(zu31100, zu4500, bda), new_esEs24(zu31101, zu4501, bdb))
new_primEqNat0(Succ(zu311000), Succ(zu45000)) → new_primEqNat0(zu311000, zu45000)
new_esEs11(GT, EQ) → False
new_esEs11(EQ, GT) → False
new_esEs17(Left(zu31100), Left(zu4500), app(ty_Ratio, de), ce) → new_esEs13(zu31100, zu4500, de)
new_esEs21(zu31102, zu4502, app(ty_[], gg)) → new_esEs14(zu31102, zu4502, gg)
new_esEs25(zu31100, zu4500, ty_Bool) → new_esEs6(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), ea, app(ty_Ratio, eh)) → new_esEs13(zu31100, zu4500, eh)
new_esEs21(zu31102, zu4502, ty_Float) → new_esEs16(zu31102, zu4502)
new_esEs25(zu31100, zu4500, app(ty_Maybe, bee)) → new_esEs8(zu31100, zu4500, bee)
new_esEs17(Left(zu31100), Left(zu4500), ty_@0, ce) → new_esEs15(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), ea, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_primEqInt(Pos(Zero), Pos(Succ(zu45000))) → False
new_primEqInt(Pos(Succ(zu311000)), Pos(Zero)) → False
new_esEs4(zu3840, zu379, app(ty_Ratio, bh)) → new_esEs13(zu3840, zu379, bh)
new_esEs22(zu31101, zu4501, ty_Ordering) → new_esEs11(zu31101, zu4501)
new_esEs22(zu31101, zu4501, app(app(ty_Either, bab), bac)) → new_esEs17(zu31101, zu4501, bab, bac)
new_esEs26(zu31100, zu4500, app(app(app(ty_@3, bgc), bgd), bge)) → new_esEs10(zu31100, zu4500, bgc, bgd, bge)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primPlusNat0(Succ(zu7800), Zero) → Succ(zu7800)
new_primPlusNat0(Zero, Succ(zu4500000)) → Succ(zu4500000)
new_esEs4(zu3840, zu379, ty_Double) → new_esEs7(zu3840, zu379)
The set Q consists of the following terms:
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Int)
new_esEs8(Just(x0), Just(x1), ty_Bool)
new_esEs22(x0, x1, ty_Double)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(Left(x0), Left(x1), ty_Int, x2)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Integer)
new_esEs13(:%(x0, x1), :%(x2, x3), x4)
new_esEs21(x0, x1, ty_Char)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs17(Left(x0), Left(x1), ty_Char, x2)
new_esEs10(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs11(EQ, LT)
new_esEs11(LT, EQ)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs8(Just(x0), Just(x1), ty_Double)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Zero, Succ(x0))
new_esEs26(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Right(x0), Right(x1), x2, ty_Bool)
new_esEs24(x0, x1, ty_Int)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs17(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs9(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs14(:(x0, x1), [], x2)
new_esEs23(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Char)
new_primPlusNat1(Zero, x0)
new_esEs4(x0, x1, ty_@0)
new_esEs20(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_asAs(True, x0)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(False, x0)
new_esEs24(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Integer)
new_sr(Pos(x0), Pos(x1))
new_esEs23(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs18(x0, x1)
new_esEs12(Char(x0), Char(x1))
new_esEs23(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Bool)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_primEqNat0(Succ(x0), Zero)
new_esEs11(EQ, GT)
new_esEs11(GT, EQ)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, ty_Integer)
new_esEs8(Nothing, Just(x0), x1)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs22(x0, x1, ty_Char)
new_esEs8(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primEqNat0(Zero, Zero)
new_primEqNat0(Zero, Succ(x0))
new_esEs17(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs15(@0, @0)
new_esEs21(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Ordering)
new_esEs17(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs6(False, False)
new_esEs4(x0, x1, ty_Integer)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Left(x0), Left(x1), ty_Float, x2)
new_esEs21(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Ordering)
new_esEs23(x0, x1, ty_Ordering)
new_esEs8(Just(x0), Just(x1), ty_Int)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(Integer(x0), Integer(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_Bool)
new_esEs14([], [], x0)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs25(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs17(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Ordering)
new_esEs17(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs26(x0, x1, ty_Integer)
new_esEs11(GT, GT)
new_esEs19(x0, x1, ty_Integer)
new_esEs16(Float(x0, x1), Float(x2, x3))
new_esEs8(Just(x0), Just(x1), ty_@0)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Right(x0), Right(x1), x2, ty_Float)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_@0)
new_esEs8(Just(x0), Just(x1), ty_Ordering)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs11(LT, GT)
new_esEs11(GT, LT)
new_esEs25(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Char)
new_primMulNat0(Succ(x0), Zero)
new_esEs19(x0, x1, ty_Int)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_esEs17(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Left(x0), Left(x1), ty_Integer, x2)
new_esEs26(x0, x1, ty_Bool)
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs17(Right(x0), Left(x1), x2, x3)
new_esEs17(Left(x0), Right(x1), x2, x3)
new_esEs4(x0, x1, ty_Float)
new_primPlusNat0(Succ(x0), Zero)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs17(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, ty_Ordering)
new_esEs17(Right(x0), Right(x1), x2, ty_@0)
new_esEs8(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_@0)
new_primPlusNat1(Succ(x0), x1)
new_esEs17(Right(x0), Right(x1), x2, ty_Int)
new_esEs21(x0, x1, ty_Ordering)
new_esEs17(Right(x0), Right(x1), x2, ty_Integer)
new_esEs21(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Double)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_sr(Neg(x0), Neg(x1))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs17(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs11(LT, LT)
new_esEs22(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs23(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Float)
new_primPlusNat0(Zero, Zero)
new_esEs8(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Nothing, Nothing, x0)
new_esEs8(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs6(True, True)
new_esEs8(Just(x0), Just(x1), ty_Float)
new_esEs4(x0, x1, ty_Char)
new_esEs14([], :(x0, x1), x2)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs21(x0, x1, ty_Int)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs17(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs11(EQ, EQ)
new_esEs8(Just(x0), Just(x1), app(ty_[], x2))
new_esEs21(x0, x1, app(ty_[], x2))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs6(False, True)
new_esEs6(True, False)
new_esEs4(x0, x1, ty_Int)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs8(Just(x0), Just(x1), ty_Char)
new_esEs17(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs17(Left(x0), Left(x1), ty_Double, x2)
new_esEs23(x0, x1, ty_Integer)
new_esEs8(Just(x0), Nothing, x1)
new_esEs17(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs23(x0, x1, ty_Bool)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(Double(x0, x1), Double(x2, x3))
new_esEs17(Right(x0), Right(x1), x2, ty_Char)
new_esEs25(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, ty_Bool)
new_esEs8(Just(x0), Just(x1), ty_Integer)
new_esEs17(Right(x0), Right(x1), x2, ty_Double)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs17(Left(x0), Left(x1), ty_@0, x2)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_nubByNubBy'10(zu379, zu380, zu381, zu382, :(zu3840, zu3841), ba) → new_nubByNubBy'1(zu379, zu380, zu381, zu382, new_esEs4(zu3840, zu379, ba), zu3841, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 > 6, 6 >= 7
- new_nubByNubBy'1(zu379, zu380, zu381, zu382, False, :(zu3840, zu3841), ba) → new_nubByNubBy'1(zu379, zu380, zu381, zu382, new_esEs4(zu3840, zu379, ba), zu3841, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 6 > 6, 7 >= 7
- new_nubByNubBy'1(zu379, :(zu3800, zu3801), zu381, zu382, True, zu384, ba) → new_nubByNubBy'10(zu3800, zu3801, zu381, zu382, :(zu381, zu382), ba)
The graph contains the following edges 2 > 1, 2 > 2, 3 >= 3, 4 >= 4, 7 >= 6
- new_nubByNubBy'1(zu379, zu380, zu381, zu382, False, [], ba) → new_nubByNubBy'(zu380, zu379, :(zu381, zu382), ba)
The graph contains the following edges 2 >= 1, 1 >= 2, 7 >= 4
- new_nubByNubBy'(:(zu3800, zu3801), zu381, zu382, ba) → new_nubByNubBy'10(zu3800, zu3801, zu381, zu382, :(zu381, zu382), ba)
The graph contains the following edges 1 > 1, 1 > 2, 2 >= 3, 3 >= 4, 4 >= 6
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy(zu3110, :(zu450, zu451), bb) → new_deleteBy0(zu451, zu450, zu3110, new_esEs27(zu3110, zu450, bb), bb)
new_deleteBy0(zu52, zu53, zu54, False, ba) → new_deleteBy(zu54, zu52, ba)
The TRS R consists of the following rules:
new_esEs25(zu31100, zu4500, app(ty_[], bed)) → new_esEs14(zu31100, zu4500, bed)
new_esEs8(Just(zu31100), Just(zu4500), app(ty_[], bbh)) → new_esEs14(zu31100, zu4500, bbh)
new_esEs27(zu3110, zu450, app(app(ty_@2, ed), ee)) → new_esEs9(zu3110, zu450, ed, ee)
new_esEs24(zu31101, zu4501, ty_@0) → new_esEs15(zu31101, zu4501)
new_esEs17(Right(zu31100), Right(zu4500), cg, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs26(zu31100, zu4500, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Char, bd) → new_esEs12(zu31100, zu4500)
new_esEs27(zu3110, zu450, app(app(ty_Either, cg), bd)) → new_esEs17(zu3110, zu450, cg, bd)
new_esEs22(zu31101, zu4501, app(ty_Ratio, hc)) → new_esEs13(zu31101, zu4501, hc)
new_esEs8(Just(zu31100), Just(zu4500), ty_Bool) → new_esEs6(zu31100, zu4500)
new_primEqInt(Neg(Succ(zu311000)), Pos(zu4500)) → False
new_primEqInt(Pos(Succ(zu311000)), Neg(zu4500)) → False
new_esEs27(zu3110, zu450, ty_Ordering) → new_esEs11(zu3110, zu450)
new_esEs24(zu31101, zu4501, app(ty_Ratio, bda)) → new_esEs13(zu31101, zu4501, bda)
new_esEs23(zu31100, zu4500, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs25(zu31100, zu4500, ty_Char) → new_esEs12(zu31100, zu4500)
new_esEs25(zu31100, zu4500, app(app(app(ty_@3, bdh), bea), beb)) → new_esEs10(zu31100, zu4500, bdh, bea, beb)
new_esEs26(zu31100, zu4500, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs24(zu31101, zu4501, ty_Ordering) → new_esEs11(zu31101, zu4501)
new_primEqInt(Neg(Zero), Pos(Succ(zu45000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(zu45000))) → False
new_esEs8(Just(zu31100), Just(zu4500), ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Float, bd) → new_esEs16(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), cg, ty_Bool) → new_esEs6(zu31100, zu4500)
new_esEs21(zu31102, zu4502, ty_Ordering) → new_esEs11(zu31102, zu4502)
new_esEs23(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs22(zu31101, zu4501, ty_Char) → new_esEs12(zu31101, zu4501)
new_esEs24(zu31101, zu4501, app(app(app(ty_@3, bcf), bcg), bch)) → new_esEs10(zu31101, zu4501, bcf, bcg, bch)
new_esEs11(EQ, EQ) → True
new_esEs23(zu31100, zu4500, ty_Float) → new_esEs16(zu31100, zu4500)
new_esEs8(Just(zu31100), Just(zu4500), ty_Float) → new_esEs16(zu31100, zu4500)
new_primMulNat0(Zero, Zero) → Zero
new_esEs27(zu3110, zu450, app(ty_Maybe, ec)) → new_esEs8(zu3110, zu450, ec)
new_esEs17(Left(zu31100), Right(zu4500), cg, bd) → False
new_esEs17(Right(zu31100), Left(zu4500), cg, bd) → False
new_esEs26(zu31100, zu4500, ty_Float) → new_esEs16(zu31100, zu4500)
new_esEs12(Char(zu31100), Char(zu4500)) → new_primEqNat0(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(ty_Ratio, bae)) → new_esEs13(zu31100, zu4500, bae)
new_esEs8(Just(zu31100), Just(zu4500), ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs21(zu31102, zu4502, ty_Integer) → new_esEs5(zu31102, zu4502)
new_esEs23(zu31100, zu4500, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs11(LT, GT) → False
new_esEs11(GT, LT) → False
new_esEs25(zu31100, zu4500, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(app(app(ty_@3, bab), bac), bad)) → new_esEs10(zu31100, zu4500, bab, bac, bad)
new_esEs25(zu31100, zu4500, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs24(zu31101, zu4501, app(ty_[], bdb)) → new_esEs14(zu31101, zu4501, bdb)
new_esEs26(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(ty_Maybe, hg)) → new_esEs8(zu31100, zu4500, hg)
new_sr(Neg(zu311000), Pos(zu45000)) → Neg(new_primMulNat0(zu311000, zu45000))
new_sr(Pos(zu311000), Neg(zu45000)) → Neg(new_primMulNat0(zu311000, zu45000))
new_esEs11(LT, EQ) → False
new_esEs11(EQ, LT) → False
new_esEs19(zu31101, zu4501, ty_Int) → new_esEs18(zu31101, zu4501)
new_esEs20(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(app(ty_@2, hh), baa)) → new_esEs9(zu31100, zu4500, hh, baa)
new_esEs5(Integer(zu31100), Integer(zu4500)) → new_primEqInt(zu31100, zu4500)
new_esEs27(zu3110, zu450, ty_@0) → new_esEs15(zu3110, zu450)
new_esEs8(Just(zu31100), Just(zu4500), app(app(app(ty_@3, bbd), bbe), bbf)) → new_esEs10(zu31100, zu4500, bbd, bbe, bbf)
new_esEs26(zu31100, zu4500, ty_Bool) → new_esEs6(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(ty_[], hd)) → new_esEs14(zu31101, zu4501, hd)
new_primEqNat0(Succ(zu311000), Zero) → False
new_primEqNat0(Zero, Succ(zu45000)) → False
new_esEs17(Right(zu31100), Right(zu4500), cg, ty_Float) → new_esEs16(zu31100, zu4500)
new_primPlusNat0(Zero, Zero) → Zero
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs26(zu31100, zu4500, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs13(:%(zu31100, zu31101), :%(zu4500, zu4501), bc) → new_asAs(new_esEs20(zu31100, zu4500, bc), new_esEs19(zu31101, zu4501, bc))
new_esEs17(Right(zu31100), Right(zu4500), cg, app(ty_[], dh)) → new_esEs14(zu31100, zu4500, dh)
new_esEs14([], [], fa) → True
new_esEs27(zu3110, zu450, ty_Int) → new_esEs18(zu3110, zu450)
new_esEs17(Left(zu31100), Left(zu4500), ty_Ordering, bd) → new_esEs11(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(app(app(ty_@3, gh), ha), hb)) → new_esEs10(zu31101, zu4501, gh, ha, hb)
new_esEs20(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), cg, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs8(Just(zu31100), Just(zu4500), ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs21(zu31102, zu4502, ty_Double) → new_esEs7(zu31102, zu4502)
new_esEs21(zu31102, zu4502, app(app(ty_Either, gc), gd)) → new_esEs17(zu31102, zu4502, gc, gd)
new_esEs17(Left(zu31100), Left(zu4500), app(app(ty_Either, ce), cf), bd) → new_esEs17(zu31100, zu4500, ce, cf)
new_esEs26(zu31100, zu4500, ty_Char) → new_esEs12(zu31100, zu4500)
new_primPlusNat1(Succ(zu780), zu450000) → Succ(Succ(new_primPlusNat0(zu780, zu450000)))
new_esEs23(zu31100, zu4500, app(ty_[], baf)) → new_esEs14(zu31100, zu4500, baf)
new_esEs22(zu31101, zu4501, ty_@0) → new_esEs15(zu31101, zu4501)
new_esEs16(Float(zu31100, zu31101), Float(zu4500, zu4501)) → new_esEs18(new_sr(zu31100, zu4500), new_sr(zu31101, zu4501))
new_esEs8(Just(zu31100), Just(zu4500), ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs23(zu31100, zu4500, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs22(zu31101, zu4501, ty_Bool) → new_esEs6(zu31101, zu4501)
new_esEs21(zu31102, zu4502, ty_Int) → new_esEs18(zu31102, zu4502)
new_esEs6(True, True) → True
new_esEs25(zu31100, zu4500, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs18(zu3110, zu450) → new_primEqInt(zu3110, zu450)
new_esEs24(zu31101, zu4501, ty_Bool) → new_esEs6(zu31101, zu4501)
new_esEs17(Left(zu31100), Left(zu4500), app(ty_[], cd), bd) → new_esEs14(zu31100, zu4500, cd)
new_esEs17(Right(zu31100), Right(zu4500), cg, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Integer, bd) → new_esEs5(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), app(ty_Maybe, be), bd) → new_esEs8(zu31100, zu4500, be)
new_esEs27(zu3110, zu450, ty_Bool) → new_esEs6(zu3110, zu450)
new_esEs22(zu31101, zu4501, ty_Double) → new_esEs7(zu31101, zu4501)
new_esEs8(Nothing, Nothing, ec) → True
new_esEs21(zu31102, zu4502, app(ty_Ratio, ga)) → new_esEs13(zu31102, zu4502, ga)
new_esEs21(zu31102, zu4502, app(app(ty_@2, fc), fd)) → new_esEs9(zu31102, zu4502, fc, fd)
new_esEs11(GT, GT) → True
new_esEs17(Right(zu31100), Right(zu4500), cg, app(app(ty_@2, db), dc)) → new_esEs9(zu31100, zu4500, db, dc)
new_sr(Neg(zu311000), Neg(zu45000)) → Pos(new_primMulNat0(zu311000, zu45000))
new_esEs15(@0, @0) → True
new_esEs24(zu31101, zu4501, app(app(ty_Either, bdc), bdd)) → new_esEs17(zu31101, zu4501, bdc, bdd)
new_esEs10(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), ef, eg, eh) → new_asAs(new_esEs23(zu31100, zu4500, ef), new_asAs(new_esEs22(zu31101, zu4501, eg), new_esEs21(zu31102, zu4502, eh)))
new_esEs22(zu31101, zu4501, app(app(ty_@2, gf), gg)) → new_esEs9(zu31101, zu4501, gf, gg)
new_esEs25(zu31100, zu4500, app(ty_Ratio, bec)) → new_esEs13(zu31100, zu4500, bec)
new_esEs25(zu31100, zu4500, app(app(ty_Either, bee), bef)) → new_esEs17(zu31100, zu4500, bee, bef)
new_asAs(False, zu68) → False
new_sr(Pos(zu311000), Pos(zu45000)) → Pos(new_primMulNat0(zu311000, zu45000))
new_esEs8(Just(zu31100), Just(zu4500), ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs22(zu31101, zu4501, ty_Int) → new_esEs18(zu31101, zu4501)
new_primEqNat0(Zero, Zero) → True
new_esEs17(Left(zu31100), Left(zu4500), ty_Bool, bd) → new_esEs6(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(ty_Maybe, ge)) → new_esEs8(zu31101, zu4501, ge)
new_primMulNat0(Zero, Succ(zu450000)) → Zero
new_primMulNat0(Succ(zu3110000), Zero) → Zero
new_esEs21(zu31102, zu4502, ty_Bool) → new_esEs6(zu31102, zu4502)
new_primMulNat0(Succ(zu3110000), Succ(zu450000)) → new_primPlusNat1(new_primMulNat0(zu3110000, Succ(zu450000)), zu450000)
new_esEs26(zu31100, zu4500, app(app(ty_@2, beh), bfa)) → new_esEs9(zu31100, zu4500, beh, bfa)
new_esEs26(zu31100, zu4500, app(ty_Ratio, bfe)) → new_esEs13(zu31100, zu4500, bfe)
new_esEs24(zu31101, zu4501, ty_Integer) → new_esEs5(zu31101, zu4501)
new_esEs27(zu3110, zu450, app(ty_Ratio, bc)) → new_esEs13(zu3110, zu450, bc)
new_esEs27(zu3110, zu450, ty_Char) → new_esEs12(zu3110, zu450)
new_esEs22(zu31101, zu4501, ty_Integer) → new_esEs5(zu31101, zu4501)
new_esEs23(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), app(app(app(ty_@3, bh), ca), cb), bd) → new_esEs10(zu31100, zu4500, bh, ca, cb)
new_esEs21(zu31102, zu4502, app(ty_Maybe, fb)) → new_esEs8(zu31102, zu4502, fb)
new_esEs27(zu3110, zu450, app(app(app(ty_@3, ef), eg), eh)) → new_esEs10(zu3110, zu450, ef, eg, eh)
new_esEs23(zu31100, zu4500, ty_Char) → new_esEs12(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Int, bd) → new_esEs18(zu31100, zu4500)
new_esEs24(zu31101, zu4501, ty_Char) → new_esEs12(zu31101, zu4501)
new_esEs26(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs25(zu31100, zu4500, ty_Float) → new_esEs16(zu31100, zu4500)
new_esEs25(zu31100, zu4500, app(app(ty_@2, bdf), bdg)) → new_esEs9(zu31100, zu4500, bdf, bdg)
new_esEs27(zu3110, zu450, ty_Integer) → new_esEs5(zu3110, zu450)
new_esEs8(Just(zu31100), Nothing, ec) → False
new_esEs8(Nothing, Just(zu4500), ec) → False
new_esEs22(zu31101, zu4501, ty_Float) → new_esEs16(zu31101, zu4501)
new_esEs24(zu31101, zu4501, ty_Double) → new_esEs7(zu31101, zu4501)
new_primEqInt(Neg(Succ(zu311000)), Neg(Succ(zu45000))) → new_primEqNat0(zu311000, zu45000)
new_esEs17(Right(zu31100), Right(zu4500), cg, app(app(app(ty_@3, dd), de), df)) → new_esEs10(zu31100, zu4500, dd, de, df)
new_esEs19(zu31101, zu4501, ty_Integer) → new_esEs5(zu31101, zu4501)
new_esEs26(zu31100, zu4500, app(ty_Maybe, beg)) → new_esEs8(zu31100, zu4500, beg)
new_esEs8(Just(zu31100), Just(zu4500), app(app(ty_@2, bbb), bbc)) → new_esEs9(zu31100, zu4500, bbb, bbc)
new_esEs17(Right(zu31100), Right(zu4500), cg, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), cg, app(app(ty_Either, ea), eb)) → new_esEs17(zu31100, zu4500, ea, eb)
new_esEs27(zu3110, zu450, ty_Double) → new_esEs7(zu3110, zu450)
new_esEs8(Just(zu31100), Just(zu4500), app(ty_Ratio, bbg)) → new_esEs13(zu31100, zu4500, bbg)
new_esEs23(zu31100, zu4500, app(app(ty_Either, bag), bah)) → new_esEs17(zu31100, zu4500, bag, bah)
new_esEs21(zu31102, zu4502, ty_Char) → new_esEs12(zu31102, zu4502)
new_esEs26(zu31100, zu4500, app(app(ty_Either, bfg), bfh)) → new_esEs17(zu31100, zu4500, bfg, bfh)
new_esEs24(zu31101, zu4501, app(ty_Maybe, bcc)) → new_esEs8(zu31101, zu4501, bcc)
new_esEs21(zu31102, zu4502, ty_@0) → new_esEs15(zu31102, zu4502)
new_esEs14(:(zu31100, zu31101), [], fa) → False
new_esEs14([], :(zu4500, zu4501), fa) → False
new_esEs25(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs8(Just(zu31100), Just(zu4500), ty_Char) → new_esEs12(zu31100, zu4500)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs26(zu31100, zu4500, app(ty_[], bff)) → new_esEs14(zu31100, zu4500, bff)
new_esEs17(Left(zu31100), Left(zu4500), app(app(ty_@2, bf), bg), bd) → new_esEs9(zu31100, zu4500, bf, bg)
new_primEqInt(Neg(Zero), Neg(Succ(zu45000))) → False
new_primEqInt(Neg(Succ(zu311000)), Neg(Zero)) → False
new_esEs17(Right(zu31100), Right(zu4500), cg, ty_Char) → new_esEs12(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), cg, app(ty_Maybe, da)) → new_esEs8(zu31100, zu4500, da)
new_esEs24(zu31101, zu4501, app(app(ty_@2, bcd), bce)) → new_esEs9(zu31101, zu4501, bcd, bce)
new_primPlusNat1(Zero, zu450000) → Succ(zu450000)
new_primPlusNat0(Succ(zu7800), Succ(zu4500000)) → Succ(Succ(new_primPlusNat0(zu7800, zu4500000)))
new_esEs21(zu31102, zu4502, app(app(app(ty_@3, ff), fg), fh)) → new_esEs10(zu31102, zu4502, ff, fg, fh)
new_esEs17(Left(zu31100), Left(zu4500), ty_Double, bd) → new_esEs7(zu31100, zu4500)
new_esEs7(Double(zu31100, zu31101), Double(zu4500, zu4501)) → new_esEs18(new_sr(zu31100, zu4500), new_sr(zu31101, zu4501))
new_esEs27(zu3110, zu450, app(ty_[], fa)) → new_esEs14(zu3110, zu450, fa)
new_esEs14(:(zu31100, zu31101), :(zu4500, zu4501), fa) → new_asAs(new_esEs26(zu31100, zu4500, fa), new_esEs14(zu31101, zu4501, fa))
new_esEs24(zu31101, zu4501, ty_Float) → new_esEs16(zu31101, zu4501)
new_asAs(True, zu68) → zu68
new_esEs27(zu3110, zu450, ty_Float) → new_esEs16(zu3110, zu450)
new_esEs11(LT, LT) → True
new_esEs8(Just(zu31100), Just(zu4500), app(ty_Maybe, bba)) → new_esEs8(zu31100, zu4500, bba)
new_esEs23(zu31100, zu4500, ty_Bool) → new_esEs6(zu31100, zu4500)
new_primEqInt(Pos(Succ(zu311000)), Pos(Succ(zu45000))) → new_primEqNat0(zu311000, zu45000)
new_esEs25(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs6(True, False) → False
new_esEs6(False, True) → False
new_esEs8(Just(zu31100), Just(zu4500), app(app(ty_Either, bca), bcb)) → new_esEs17(zu31100, zu4500, bca, bcb)
new_esEs24(zu31101, zu4501, ty_Int) → new_esEs18(zu31101, zu4501)
new_esEs6(False, False) → True
new_esEs9(@2(zu31100, zu31101), @2(zu4500, zu4501), ed, ee) → new_asAs(new_esEs25(zu31100, zu4500, ed), new_esEs24(zu31101, zu4501, ee))
new_primEqNat0(Succ(zu311000), Succ(zu45000)) → new_primEqNat0(zu311000, zu45000)
new_esEs11(EQ, GT) → False
new_esEs11(GT, EQ) → False
new_esEs17(Left(zu31100), Left(zu4500), app(ty_Ratio, cc), bd) → new_esEs13(zu31100, zu4500, cc)
new_esEs21(zu31102, zu4502, app(ty_[], gb)) → new_esEs14(zu31102, zu4502, gb)
new_esEs25(zu31100, zu4500, ty_Bool) → new_esEs6(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), cg, app(ty_Ratio, dg)) → new_esEs13(zu31100, zu4500, dg)
new_esEs21(zu31102, zu4502, ty_Float) → new_esEs16(zu31102, zu4502)
new_esEs25(zu31100, zu4500, app(ty_Maybe, bde)) → new_esEs8(zu31100, zu4500, bde)
new_esEs17(Left(zu31100), Left(zu4500), ty_@0, bd) → new_esEs15(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), cg, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_primEqInt(Pos(Zero), Pos(Succ(zu45000))) → False
new_primEqInt(Pos(Succ(zu311000)), Pos(Zero)) → False
new_esEs22(zu31101, zu4501, ty_Ordering) → new_esEs11(zu31101, zu4501)
new_esEs22(zu31101, zu4501, app(app(ty_Either, he), hf)) → new_esEs17(zu31101, zu4501, he, hf)
new_esEs26(zu31100, zu4500, app(app(app(ty_@3, bfb), bfc), bfd)) → new_esEs10(zu31100, zu4500, bfb, bfc, bfd)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primPlusNat0(Zero, Succ(zu4500000)) → Succ(zu4500000)
new_primPlusNat0(Succ(zu7800), Zero) → Succ(zu7800)
The set Q consists of the following terms:
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, ty_Int)
new_esEs8(Just(x0), Just(x1), ty_Bool)
new_esEs22(x0, x1, ty_Double)
new_esEs17(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs17(Left(x0), Left(x1), ty_Double, x2)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs17(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, ty_Integer)
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Integer)
new_esEs17(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs21(x0, x1, ty_Char)
new_esEs27(x0, x1, ty_Int)
new_esEs17(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs8(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs17(Right(x0), Right(x1), x2, ty_Double)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Just(x0), Nothing, x1)
new_esEs11(LT, EQ)
new_esEs11(EQ, LT)
new_esEs14([], :(x0, x1), x2)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs8(Just(x0), Just(x1), ty_Double)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_primPlusNat0(Zero, Succ(x0))
new_esEs13(:%(x0, x1), :%(x2, x3), x4)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs10(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs17(Left(x0), Left(x1), ty_Integer, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, ty_Int)
new_esEs17(Right(x0), Right(x1), x2, ty_Integer)
new_esEs17(Left(x0), Left(x1), ty_Int, x2)
new_esEs14([], [], x0)
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_esEs27(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs27(x0, x1, ty_Float)
new_esEs27(x0, x1, ty_@0)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Char)
new_primPlusNat1(Zero, x0)
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs17(Left(x0), Left(x1), ty_Float, x2)
new_esEs20(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Float)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, ty_Ordering)
new_asAs(True, x0)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs8(Just(x0), Just(x1), app(ty_[], x2))
new_asAs(False, x0)
new_esEs24(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, ty_Integer)
new_esEs27(x0, x1, ty_Double)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_sr(Pos(x0), Pos(x1))
new_esEs17(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs23(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs18(x0, x1)
new_esEs12(Char(x0), Char(x1))
new_esEs23(x0, x1, ty_Float)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_Double)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Bool)
new_esEs17(Left(x0), Left(x1), ty_Bool, x2)
new_primEqNat0(Succ(x0), Zero)
new_esEs11(GT, EQ)
new_esEs11(EQ, GT)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, ty_Integer)
new_esEs8(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs17(Right(x0), Right(x1), x2, ty_Int)
new_esEs9(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs22(x0, x1, ty_Char)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs17(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primEqNat0(Zero, Zero)
new_primEqNat0(Zero, Succ(x0))
new_esEs15(@0, @0)
new_esEs21(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Ordering)
new_esEs6(False, False)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Ordering)
new_esEs23(x0, x1, ty_Ordering)
new_esEs8(Just(x0), Just(x1), ty_Int)
new_esEs5(Integer(x0), Integer(x1))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs22(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs24(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Double)
new_esEs8(Nothing, Just(x0), x1)
new_esEs8(Nothing, Nothing, x0)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Char)
new_esEs8(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, ty_Ordering)
new_esEs17(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs26(x0, x1, ty_Integer)
new_esEs11(GT, GT)
new_esEs8(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs17(Right(x0), Right(x1), x2, ty_Char)
new_esEs19(x0, x1, ty_Integer)
new_esEs16(Float(x0, x1), Float(x2, x3))
new_esEs17(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs8(Just(x0), Just(x1), ty_@0)
new_esEs17(Right(x0), Right(x1), x2, ty_Bool)
new_esEs17(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs22(x0, x1, ty_@0)
new_esEs8(Just(x0), Just(x1), ty_Ordering)
new_esEs11(GT, LT)
new_esEs11(LT, GT)
new_esEs25(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Right(x0), Right(x1), x2, ty_@0)
new_esEs27(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Char)
new_primMulNat0(Succ(x0), Zero)
new_esEs19(x0, x1, ty_Int)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, ty_Bool)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs17(Right(x0), Left(x1), x2, x3)
new_esEs17(Left(x0), Right(x1), x2, x3)
new_primPlusNat0(Succ(x0), Zero)
new_esEs17(Left(x0), Left(x1), ty_Char, x2)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_@0)
new_primPlusNat1(Succ(x0), x1)
new_esEs17(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Right(x0), Right(x1), x2, ty_Float)
new_esEs21(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Bool)
new_sr(Neg(x0), Neg(x1))
new_esEs17(Left(x0), Left(x1), ty_@0, x2)
new_esEs11(LT, LT)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs23(x0, x1, ty_Int)
new_esEs14(:(x0, x1), [], x2)
new_esEs21(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat0(Zero, Zero)
new_esEs17(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs8(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(True, True)
new_esEs8(Just(x0), Just(x1), ty_Float)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_sr(Neg(x0), Pos(x1))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Neg(x1))
new_esEs21(x0, x1, ty_Int)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs17(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs11(EQ, EQ)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs6(False, True)
new_esEs6(True, False)
new_esEs8(Just(x0), Just(x1), ty_Char)
new_esEs27(x0, x1, ty_Char)
new_esEs23(x0, x1, ty_Integer)
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Bool)
new_esEs7(Double(x0, x1), Double(x2, x3))
new_esEs25(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Just(x0), Just(x1), ty_Integer)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_deleteBy0(zu52, zu53, zu54, False, ba) → new_deleteBy(zu54, zu52, ba)
The graph contains the following edges 3 >= 1, 1 >= 2, 5 >= 3
- new_deleteBy(zu3110, :(zu450, zu451), bb) → new_deleteBy0(zu451, zu450, zu3110, new_esEs27(zu3110, zu450, bb), bb)
The graph contains the following edges 2 > 1, 2 > 2, 1 >= 3, 3 >= 5
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_foldl(zu45, :(zu3110, zu3111), ba) → new_foldl(new_deleteBy1(zu3110, zu45, ba), zu3111, ba)
The TRS R consists of the following rules:
new_esEs25(zu31100, zu4500, app(ty_[], bec)) → new_esEs14(zu31100, zu4500, bec)
new_esEs8(Just(zu31100), Just(zu4500), app(ty_[], bbg)) → new_esEs14(zu31100, zu4500, bbg)
new_esEs27(zu3110, zu450, app(app(ty_@2, ec), ed)) → new_esEs9(zu3110, zu450, ec, ed)
new_esEs24(zu31101, zu4501, ty_@0) → new_esEs15(zu31101, zu4501)
new_esEs17(Right(zu31100), Right(zu4500), cf, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs26(zu31100, zu4500, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Char, bc) → new_esEs12(zu31100, zu4500)
new_esEs27(zu3110, zu450, app(app(ty_Either, cf), bc)) → new_esEs17(zu3110, zu450, cf, bc)
new_esEs22(zu31101, zu4501, app(ty_Ratio, hb)) → new_esEs13(zu31101, zu4501, hb)
new_esEs8(Just(zu31100), Just(zu4500), ty_Bool) → new_esEs6(zu31100, zu4500)
new_primEqInt(Neg(Succ(zu311000)), Pos(zu4500)) → False
new_primEqInt(Pos(Succ(zu311000)), Neg(zu4500)) → False
new_esEs27(zu3110, zu450, ty_Ordering) → new_esEs11(zu3110, zu450)
new_esEs24(zu31101, zu4501, app(ty_Ratio, bch)) → new_esEs13(zu31101, zu4501, bch)
new_esEs23(zu31100, zu4500, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs25(zu31100, zu4500, ty_Char) → new_esEs12(zu31100, zu4500)
new_esEs25(zu31100, zu4500, app(app(app(ty_@3, bdg), bdh), bea)) → new_esEs10(zu31100, zu4500, bdg, bdh, bea)
new_esEs26(zu31100, zu4500, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs24(zu31101, zu4501, ty_Ordering) → new_esEs11(zu31101, zu4501)
new_primEqInt(Neg(Zero), Pos(Succ(zu45000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(zu45000))) → False
new_esEs8(Just(zu31100), Just(zu4500), ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Float, bc) → new_esEs16(zu31100, zu4500)
new_deleteBy00(zu52, zu53, zu54, False, bef) → :(zu53, new_deleteBy1(zu54, zu52, bef))
new_esEs17(Right(zu31100), Right(zu4500), cf, ty_Bool) → new_esEs6(zu31100, zu4500)
new_esEs21(zu31102, zu4502, ty_Ordering) → new_esEs11(zu31102, zu4502)
new_esEs23(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs22(zu31101, zu4501, ty_Char) → new_esEs12(zu31101, zu4501)
new_esEs24(zu31101, zu4501, app(app(app(ty_@3, bce), bcf), bcg)) → new_esEs10(zu31101, zu4501, bce, bcf, bcg)
new_esEs11(EQ, EQ) → True
new_esEs23(zu31100, zu4500, ty_Float) → new_esEs16(zu31100, zu4500)
new_deleteBy1(zu3110, :(zu450, zu451), ba) → new_deleteBy00(zu451, zu450, zu3110, new_esEs27(zu3110, zu450, ba), ba)
new_esEs8(Just(zu31100), Just(zu4500), ty_Float) → new_esEs16(zu31100, zu4500)
new_primMulNat0(Zero, Zero) → Zero
new_esEs27(zu3110, zu450, app(ty_Maybe, eb)) → new_esEs8(zu3110, zu450, eb)
new_esEs17(Left(zu31100), Right(zu4500), cf, bc) → False
new_esEs17(Right(zu31100), Left(zu4500), cf, bc) → False
new_esEs26(zu31100, zu4500, ty_Float) → new_esEs16(zu31100, zu4500)
new_esEs12(Char(zu31100), Char(zu4500)) → new_primEqNat0(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(ty_Ratio, bad)) → new_esEs13(zu31100, zu4500, bad)
new_esEs8(Just(zu31100), Just(zu4500), ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs21(zu31102, zu4502, ty_Integer) → new_esEs5(zu31102, zu4502)
new_esEs23(zu31100, zu4500, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs11(LT, GT) → False
new_esEs11(GT, LT) → False
new_esEs25(zu31100, zu4500, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(app(app(ty_@3, baa), bab), bac)) → new_esEs10(zu31100, zu4500, baa, bab, bac)
new_esEs25(zu31100, zu4500, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs24(zu31101, zu4501, app(ty_[], bda)) → new_esEs14(zu31101, zu4501, bda)
new_esEs26(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(ty_Maybe, hf)) → new_esEs8(zu31100, zu4500, hf)
new_sr(Neg(zu311000), Pos(zu45000)) → Neg(new_primMulNat0(zu311000, zu45000))
new_sr(Pos(zu311000), Neg(zu45000)) → Neg(new_primMulNat0(zu311000, zu45000))
new_esEs11(LT, EQ) → False
new_esEs11(EQ, LT) → False
new_esEs19(zu31101, zu4501, ty_Int) → new_esEs18(zu31101, zu4501)
new_esEs20(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs23(zu31100, zu4500, app(app(ty_@2, hg), hh)) → new_esEs9(zu31100, zu4500, hg, hh)
new_esEs5(Integer(zu31100), Integer(zu4500)) → new_primEqInt(zu31100, zu4500)
new_esEs27(zu3110, zu450, ty_@0) → new_esEs15(zu3110, zu450)
new_esEs8(Just(zu31100), Just(zu4500), app(app(app(ty_@3, bbc), bbd), bbe)) → new_esEs10(zu31100, zu4500, bbc, bbd, bbe)
new_esEs26(zu31100, zu4500, ty_Bool) → new_esEs6(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(ty_[], hc)) → new_esEs14(zu31101, zu4501, hc)
new_primEqNat0(Succ(zu311000), Zero) → False
new_primEqNat0(Zero, Succ(zu45000)) → False
new_esEs17(Right(zu31100), Right(zu4500), cf, ty_Float) → new_esEs16(zu31100, zu4500)
new_primPlusNat0(Zero, Zero) → Zero
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs26(zu31100, zu4500, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_esEs13(:%(zu31100, zu31101), :%(zu4500, zu4501), bb) → new_asAs(new_esEs20(zu31100, zu4500, bb), new_esEs19(zu31101, zu4501, bb))
new_esEs17(Right(zu31100), Right(zu4500), cf, app(ty_[], dg)) → new_esEs14(zu31100, zu4500, dg)
new_esEs14([], [], eh) → True
new_esEs27(zu3110, zu450, ty_Int) → new_esEs18(zu3110, zu450)
new_esEs17(Left(zu31100), Left(zu4500), ty_Ordering, bc) → new_esEs11(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(app(app(ty_@3, gg), gh), ha)) → new_esEs10(zu31101, zu4501, gg, gh, ha)
new_esEs20(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), cf, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs8(Just(zu31100), Just(zu4500), ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs21(zu31102, zu4502, ty_Double) → new_esEs7(zu31102, zu4502)
new_esEs21(zu31102, zu4502, app(app(ty_Either, gb), gc)) → new_esEs17(zu31102, zu4502, gb, gc)
new_esEs17(Left(zu31100), Left(zu4500), app(app(ty_Either, cd), ce), bc) → new_esEs17(zu31100, zu4500, cd, ce)
new_esEs26(zu31100, zu4500, ty_Char) → new_esEs12(zu31100, zu4500)
new_primPlusNat1(Succ(zu780), zu450000) → Succ(Succ(new_primPlusNat0(zu780, zu450000)))
new_esEs23(zu31100, zu4500, app(ty_[], bae)) → new_esEs14(zu31100, zu4500, bae)
new_esEs22(zu31101, zu4501, ty_@0) → new_esEs15(zu31101, zu4501)
new_esEs16(Float(zu31100, zu31101), Float(zu4500, zu4501)) → new_esEs18(new_sr(zu31100, zu4500), new_sr(zu31101, zu4501))
new_esEs8(Just(zu31100), Just(zu4500), ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs23(zu31100, zu4500, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs22(zu31101, zu4501, ty_Bool) → new_esEs6(zu31101, zu4501)
new_esEs21(zu31102, zu4502, ty_Int) → new_esEs18(zu31102, zu4502)
new_esEs6(True, True) → True
new_esEs25(zu31100, zu4500, ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs18(zu3110, zu450) → new_primEqInt(zu3110, zu450)
new_esEs24(zu31101, zu4501, ty_Bool) → new_esEs6(zu31101, zu4501)
new_esEs17(Left(zu31100), Left(zu4500), app(ty_[], cc), bc) → new_esEs14(zu31100, zu4500, cc)
new_esEs17(Right(zu31100), Right(zu4500), cf, ty_@0) → new_esEs15(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Integer, bc) → new_esEs5(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), app(ty_Maybe, bd), bc) → new_esEs8(zu31100, zu4500, bd)
new_esEs27(zu3110, zu450, ty_Bool) → new_esEs6(zu3110, zu450)
new_esEs22(zu31101, zu4501, ty_Double) → new_esEs7(zu31101, zu4501)
new_esEs8(Nothing, Nothing, eb) → True
new_esEs21(zu31102, zu4502, app(ty_Ratio, fh)) → new_esEs13(zu31102, zu4502, fh)
new_esEs21(zu31102, zu4502, app(app(ty_@2, fb), fc)) → new_esEs9(zu31102, zu4502, fb, fc)
new_esEs11(GT, GT) → True
new_esEs17(Right(zu31100), Right(zu4500), cf, app(app(ty_@2, da), db)) → new_esEs9(zu31100, zu4500, da, db)
new_sr(Neg(zu311000), Neg(zu45000)) → Pos(new_primMulNat0(zu311000, zu45000))
new_esEs15(@0, @0) → True
new_esEs24(zu31101, zu4501, app(app(ty_Either, bdb), bdc)) → new_esEs17(zu31101, zu4501, bdb, bdc)
new_esEs10(@3(zu31100, zu31101, zu31102), @3(zu4500, zu4501, zu4502), ee, ef, eg) → new_asAs(new_esEs23(zu31100, zu4500, ee), new_asAs(new_esEs22(zu31101, zu4501, ef), new_esEs21(zu31102, zu4502, eg)))
new_esEs22(zu31101, zu4501, app(app(ty_@2, ge), gf)) → new_esEs9(zu31101, zu4501, ge, gf)
new_esEs25(zu31100, zu4500, app(ty_Ratio, beb)) → new_esEs13(zu31100, zu4500, beb)
new_esEs25(zu31100, zu4500, app(app(ty_Either, bed), bee)) → new_esEs17(zu31100, zu4500, bed, bee)
new_asAs(False, zu68) → False
new_sr(Pos(zu311000), Pos(zu45000)) → Pos(new_primMulNat0(zu311000, zu45000))
new_esEs8(Just(zu31100), Just(zu4500), ty_Double) → new_esEs7(zu31100, zu4500)
new_esEs22(zu31101, zu4501, ty_Int) → new_esEs18(zu31101, zu4501)
new_primEqNat0(Zero, Zero) → True
new_esEs17(Left(zu31100), Left(zu4500), ty_Bool, bc) → new_esEs6(zu31100, zu4500)
new_esEs22(zu31101, zu4501, app(ty_Maybe, gd)) → new_esEs8(zu31101, zu4501, gd)
new_primMulNat0(Zero, Succ(zu450000)) → Zero
new_primMulNat0(Succ(zu3110000), Zero) → Zero
new_esEs21(zu31102, zu4502, ty_Bool) → new_esEs6(zu31102, zu4502)
new_primMulNat0(Succ(zu3110000), Succ(zu450000)) → new_primPlusNat1(new_primMulNat0(zu3110000, Succ(zu450000)), zu450000)
new_esEs26(zu31100, zu4500, app(app(ty_@2, beh), bfa)) → new_esEs9(zu31100, zu4500, beh, bfa)
new_esEs26(zu31100, zu4500, app(ty_Ratio, bfe)) → new_esEs13(zu31100, zu4500, bfe)
new_esEs24(zu31101, zu4501, ty_Integer) → new_esEs5(zu31101, zu4501)
new_esEs27(zu3110, zu450, app(ty_Ratio, bb)) → new_esEs13(zu3110, zu450, bb)
new_esEs27(zu3110, zu450, ty_Char) → new_esEs12(zu3110, zu450)
new_esEs22(zu31101, zu4501, ty_Integer) → new_esEs5(zu31101, zu4501)
new_esEs23(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), app(app(app(ty_@3, bg), bh), ca), bc) → new_esEs10(zu31100, zu4500, bg, bh, ca)
new_esEs21(zu31102, zu4502, app(ty_Maybe, fa)) → new_esEs8(zu31102, zu4502, fa)
new_esEs27(zu3110, zu450, app(app(app(ty_@3, ee), ef), eg)) → new_esEs10(zu3110, zu450, ee, ef, eg)
new_esEs23(zu31100, zu4500, ty_Char) → new_esEs12(zu31100, zu4500)
new_esEs17(Left(zu31100), Left(zu4500), ty_Int, bc) → new_esEs18(zu31100, zu4500)
new_esEs24(zu31101, zu4501, ty_Char) → new_esEs12(zu31101, zu4501)
new_esEs26(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs25(zu31100, zu4500, ty_Float) → new_esEs16(zu31100, zu4500)
new_esEs25(zu31100, zu4500, app(app(ty_@2, bde), bdf)) → new_esEs9(zu31100, zu4500, bde, bdf)
new_esEs27(zu3110, zu450, ty_Integer) → new_esEs5(zu3110, zu450)
new_esEs8(Just(zu31100), Nothing, eb) → False
new_esEs8(Nothing, Just(zu4500), eb) → False
new_esEs22(zu31101, zu4501, ty_Float) → new_esEs16(zu31101, zu4501)
new_esEs24(zu31101, zu4501, ty_Double) → new_esEs7(zu31101, zu4501)
new_primEqInt(Neg(Succ(zu311000)), Neg(Succ(zu45000))) → new_primEqNat0(zu311000, zu45000)
new_esEs17(Right(zu31100), Right(zu4500), cf, app(app(app(ty_@3, dc), dd), de)) → new_esEs10(zu31100, zu4500, dc, dd, de)
new_esEs19(zu31101, zu4501, ty_Integer) → new_esEs5(zu31101, zu4501)
new_esEs26(zu31100, zu4500, app(ty_Maybe, beg)) → new_esEs8(zu31100, zu4500, beg)
new_esEs8(Just(zu31100), Just(zu4500), app(app(ty_@2, bba), bbb)) → new_esEs9(zu31100, zu4500, bba, bbb)
new_esEs17(Right(zu31100), Right(zu4500), cf, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), cf, app(app(ty_Either, dh), ea)) → new_esEs17(zu31100, zu4500, dh, ea)
new_esEs27(zu3110, zu450, ty_Double) → new_esEs7(zu3110, zu450)
new_esEs8(Just(zu31100), Just(zu4500), app(ty_Ratio, bbf)) → new_esEs13(zu31100, zu4500, bbf)
new_esEs23(zu31100, zu4500, app(app(ty_Either, baf), bag)) → new_esEs17(zu31100, zu4500, baf, bag)
new_esEs21(zu31102, zu4502, ty_Char) → new_esEs12(zu31102, zu4502)
new_esEs26(zu31100, zu4500, app(app(ty_Either, bfg), bfh)) → new_esEs17(zu31100, zu4500, bfg, bfh)
new_esEs24(zu31101, zu4501, app(ty_Maybe, bcb)) → new_esEs8(zu31101, zu4501, bcb)
new_esEs21(zu31102, zu4502, ty_@0) → new_esEs15(zu31102, zu4502)
new_esEs14(:(zu31100, zu31101), [], eh) → False
new_esEs14([], :(zu4500, zu4501), eh) → False
new_esEs25(zu31100, zu4500, ty_Int) → new_esEs18(zu31100, zu4500)
new_esEs8(Just(zu31100), Just(zu4500), ty_Char) → new_esEs12(zu31100, zu4500)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs26(zu31100, zu4500, app(ty_[], bff)) → new_esEs14(zu31100, zu4500, bff)
new_esEs17(Left(zu31100), Left(zu4500), app(app(ty_@2, be), bf), bc) → new_esEs9(zu31100, zu4500, be, bf)
new_primEqInt(Neg(Zero), Neg(Succ(zu45000))) → False
new_primEqInt(Neg(Succ(zu311000)), Neg(Zero)) → False
new_esEs17(Right(zu31100), Right(zu4500), cf, ty_Char) → new_esEs12(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), cf, app(ty_Maybe, cg)) → new_esEs8(zu31100, zu4500, cg)
new_esEs24(zu31101, zu4501, app(app(ty_@2, bcc), bcd)) → new_esEs9(zu31101, zu4501, bcc, bcd)
new_primPlusNat1(Zero, zu450000) → Succ(zu450000)
new_primPlusNat0(Succ(zu7800), Succ(zu4500000)) → Succ(Succ(new_primPlusNat0(zu7800, zu4500000)))
new_esEs21(zu31102, zu4502, app(app(app(ty_@3, fd), ff), fg)) → new_esEs10(zu31102, zu4502, fd, ff, fg)
new_esEs17(Left(zu31100), Left(zu4500), ty_Double, bc) → new_esEs7(zu31100, zu4500)
new_deleteBy1(zu3110, [], ba) → []
new_esEs7(Double(zu31100, zu31101), Double(zu4500, zu4501)) → new_esEs18(new_sr(zu31100, zu4500), new_sr(zu31101, zu4501))
new_esEs27(zu3110, zu450, app(ty_[], eh)) → new_esEs14(zu3110, zu450, eh)
new_esEs14(:(zu31100, zu31101), :(zu4500, zu4501), eh) → new_asAs(new_esEs26(zu31100, zu4500, eh), new_esEs14(zu31101, zu4501, eh))
new_esEs24(zu31101, zu4501, ty_Float) → new_esEs16(zu31101, zu4501)
new_asAs(True, zu68) → zu68
new_esEs27(zu3110, zu450, ty_Float) → new_esEs16(zu3110, zu450)
new_esEs11(LT, LT) → True
new_esEs8(Just(zu31100), Just(zu4500), app(ty_Maybe, bah)) → new_esEs8(zu31100, zu4500, bah)
new_esEs23(zu31100, zu4500, ty_Bool) → new_esEs6(zu31100, zu4500)
new_primEqInt(Pos(Succ(zu311000)), Pos(Succ(zu45000))) → new_primEqNat0(zu311000, zu45000)
new_esEs25(zu31100, zu4500, ty_Integer) → new_esEs5(zu31100, zu4500)
new_esEs6(True, False) → False
new_esEs6(False, True) → False
new_esEs8(Just(zu31100), Just(zu4500), app(app(ty_Either, bbh), bca)) → new_esEs17(zu31100, zu4500, bbh, bca)
new_deleteBy00(zu52, zu53, zu54, True, bef) → zu52
new_esEs24(zu31101, zu4501, ty_Int) → new_esEs18(zu31101, zu4501)
new_esEs6(False, False) → True
new_esEs9(@2(zu31100, zu31101), @2(zu4500, zu4501), ec, ed) → new_asAs(new_esEs25(zu31100, zu4500, ec), new_esEs24(zu31101, zu4501, ed))
new_primEqNat0(Succ(zu311000), Succ(zu45000)) → new_primEqNat0(zu311000, zu45000)
new_esEs11(EQ, GT) → False
new_esEs11(GT, EQ) → False
new_esEs17(Left(zu31100), Left(zu4500), app(ty_Ratio, cb), bc) → new_esEs13(zu31100, zu4500, cb)
new_esEs21(zu31102, zu4502, app(ty_[], ga)) → new_esEs14(zu31102, zu4502, ga)
new_esEs25(zu31100, zu4500, ty_Bool) → new_esEs6(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), cf, app(ty_Ratio, df)) → new_esEs13(zu31100, zu4500, df)
new_esEs21(zu31102, zu4502, ty_Float) → new_esEs16(zu31102, zu4502)
new_esEs25(zu31100, zu4500, app(ty_Maybe, bdd)) → new_esEs8(zu31100, zu4500, bdd)
new_esEs17(Left(zu31100), Left(zu4500), ty_@0, bc) → new_esEs15(zu31100, zu4500)
new_esEs17(Right(zu31100), Right(zu4500), cf, ty_Ordering) → new_esEs11(zu31100, zu4500)
new_primEqInt(Pos(Zero), Pos(Succ(zu45000))) → False
new_primEqInt(Pos(Succ(zu311000)), Pos(Zero)) → False
new_esEs22(zu31101, zu4501, ty_Ordering) → new_esEs11(zu31101, zu4501)
new_esEs22(zu31101, zu4501, app(app(ty_Either, hd), he)) → new_esEs17(zu31101, zu4501, hd, he)
new_esEs26(zu31100, zu4500, app(app(app(ty_@3, bfb), bfc), bfd)) → new_esEs10(zu31100, zu4500, bfb, bfc, bfd)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primPlusNat0(Zero, Succ(zu4500000)) → Succ(zu4500000)
new_primPlusNat0(Succ(zu7800), Zero) → Succ(zu7800)
The set Q consists of the following terms:
new_primMulNat0(Succ(x0), Succ(x1))
new_deleteBy1(x0, [], x1)
new_esEs25(x0, x1, ty_Int)
new_esEs8(Just(x0), Just(x1), ty_Bool)
new_esEs22(x0, x1, ty_Double)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs8(Nothing, Nothing, x0)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs17(Right(x0), Right(x1), x2, ty_@0)
new_esEs25(x0, x1, ty_Integer)
new_deleteBy00(x0, x1, x2, True, x3)
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Char)
new_esEs27(x0, x1, ty_Int)
new_esEs17(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs8(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs17(Right(x0), Right(x1), x2, ty_Float)
new_esEs8(Nothing, Just(x0), x1)
new_esEs11(LT, EQ)
new_esEs11(EQ, LT)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs8(Just(x0), Just(x1), ty_Double)
new_esEs17(Left(x0), Left(x1), ty_Char, x2)
new_esEs14(:(x0, x1), [], x2)
new_primPlusNat0(Zero, Succ(x0))
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Char)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs8(Just(x0), Nothing, x1)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Int)
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, ty_Integer)
new_esEs17(Left(x0), Left(x1), ty_Float, x2)
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Float)
new_esEs17(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs27(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Char)
new_primPlusNat1(Zero, x0)
new_esEs20(x0, x1, ty_Int)
new_esEs17(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs26(x0, x1, ty_Float)
new_esEs25(x0, x1, ty_Ordering)
new_asAs(True, x0)
new_esEs17(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_asAs(False, x0)
new_esEs17(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs24(x0, x1, ty_Bool)
new_esEs17(Right(x0), Right(x1), x2, ty_Integer)
new_esEs24(x0, x1, ty_Integer)
new_esEs27(x0, x1, ty_Double)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Pos(x1))
new_esEs17(Right(x0), Left(x1), x2, x3)
new_esEs17(Left(x0), Right(x1), x2, x3)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Double)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs17(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs18(x0, x1)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs12(Char(x0), Char(x1))
new_esEs23(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs17(Left(x0), Left(x1), ty_Ordering, x2)
new_primEqNat0(Succ(x0), Zero)
new_esEs11(EQ, GT)
new_esEs11(GT, EQ)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs17(Left(x0), Left(x1), ty_Double, x2)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs8(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs17(Right(x0), Right(x1), x2, ty_Bool)
new_esEs22(x0, x1, ty_Char)
new_esEs8(Just(x0), Just(x1), app(ty_[], x2))
new_esEs8(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Zero)
new_primEqNat0(Zero, Succ(x0))
new_esEs15(@0, @0)
new_esEs21(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Ordering)
new_esEs6(False, False)
new_esEs17(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Ordering)
new_esEs23(x0, x1, ty_Ordering)
new_esEs8(Just(x0), Just(x1), ty_Int)
new_esEs5(Integer(x0), Integer(x1))
new_esEs17(Right(x0), Right(x1), x2, ty_Double)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs22(x0, x1, ty_Bool)
new_esEs17(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs25(x0, x1, ty_@0)
new_primMulNat0(Zero, Zero)
new_esEs17(Left(x0), Left(x1), ty_Int, x2)
new_esEs24(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Double)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs14([], [], x0)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Char)
new_esEs17(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Integer)
new_esEs17(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(GT, GT)
new_esEs19(x0, x1, ty_Integer)
new_esEs16(Float(x0, x1), Float(x2, x3))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs17(Left(x0), Left(x1), ty_@0, x2)
new_esEs8(Just(x0), Just(x1), ty_@0)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs17(Left(x0), Left(x1), ty_Integer, x2)
new_esEs8(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_@0)
new_esEs8(Just(x0), Just(x1), ty_Ordering)
new_esEs11(GT, LT)
new_esEs11(LT, GT)
new_esEs9(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs25(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Right(x0), Right(x1), x2, ty_Char)
new_esEs27(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Char)
new_esEs21(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Zero)
new_esEs19(x0, x1, ty_Int)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Bool)
new_esEs26(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_deleteBy1(x0, :(x1, x2), x3)
new_primPlusNat0(Succ(x0), Zero)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_@0)
new_primPlusNat1(Succ(x0), x1)
new_esEs17(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Ordering)
new_esEs21(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, ty_Bool)
new_sr(Neg(x0), Neg(x1))
new_esEs17(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs11(LT, LT)
new_esEs22(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs14([], :(x0, x1), x2)
new_esEs23(x0, x1, ty_Int)
new_esEs8(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs13(:%(x0, x1), :%(x2, x3), x4)
new_esEs21(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_Float)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat0(Zero, Zero)
new_esEs6(True, True)
new_esEs8(Just(x0), Just(x1), ty_Float)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs21(x0, x1, ty_Int)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs11(EQ, EQ)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs6(False, True)
new_esEs6(True, False)
new_deleteBy00(x0, x1, x2, False, x3)
new_esEs8(Just(x0), Just(x1), ty_Char)
new_esEs17(Right(x0), Right(x1), x2, ty_Int)
new_esEs27(x0, x1, ty_Char)
new_esEs23(x0, x1, ty_Integer)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, ty_Bool)
new_esEs7(Double(x0, x1), Double(x2, x3))
new_esEs25(x0, x1, ty_Bool)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Just(x0), Just(x1), ty_Integer)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldl(zu45, :(zu3110, zu3111), ba) → new_foldl(new_deleteBy1(zu3110, zu45, ba), zu3111, ba)
The graph contains the following edges 2 > 2, 3 >= 3
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_psPs(:(zu311111110, zu311111111), zu42, ba) → new_psPs(zu311111111, zu42, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs(:(zu311111110, zu311111111), zu42, ba) → new_psPs(zu311111111, zu42, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3